A language for compositional specification and verification of finite state hardware controllers
A language for compositional specification and verification of finite state hardware controllers
复制标题
一种用于有限状态硬件控制器的组合规范和验证的语言
DOI：
--
复制
发表时间：
1991
影响因子：
20.6
通讯作者：
K. McMillan
中科院分区：
文献类型：
--
作者：
E. Clarke;D. E. Long;K. McMillan
考虑了描述复杂有限状态硬件控制器的状态机语言(SML)。它提供了现代编程语言中的许多标准控制结构。由SML编译器产生的状态表可以用作时态逻辑模型检查器的输入，该时态逻辑模型检查器可以自动确定是否满足逻辑CTL中的规范。作者描述了用于模块化控制器设计的SML的扩展。这些扩展允许使用组合方法进行模型检查，这可以大大降低其复杂性。为了演示这些方法，作者讨论了一个简单的中央处理单元(CPU)控制器的规范和验证。>；
The authors consider the state machine language (SML) for describing complex finite state hardware controllers. It provides many of the standard control structures found in modern programming languages. The state tables produced by the SML compiler can be used as input to a temporal logic model checker that can automatically determine whether a specification in the logic CTL is satisfied. The authors describe extensions to SML for the design of modular controllers. These extensions allow a compositional approach to model checking which can substantially reduce its complexity. To demonstrate these methods, the authors discuss the specification and verification of a simple central-processing-unit (CPU) controller. >