Model Checking
Model Checking
复制标题
DOI：
10.1016/b978-044450813-3/50026-6
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
E. Clarke;Holger Schlingloff
中科院分区：
文献类型：
--
作者：
E. Clarke;Holger Schlingloff
模型检查是一种用于验证有限状态无功系统的自动技术，例如顺序电路设计和通信协议。规范用时间逻辑表示，反应系统被建模为状态转换图。使用一个有效的搜索过程来确定状态转移图是否满足规范。我们描述了基本的模型检查算法，并展示了如何将其与二元决策图一起使用来验证大型状态转移图的属性。我们通过验证航天飞机的部分应急制导要求来说明模型检查在发现细微错误方面的力量。
Model checking is an automatic technique for verifying finite-state reactive systems, such as sequential circuit designs and communication protocols. Specifications are expressed in temporal logic, and the reactive system is modeled as a statetransition graph. An efficient search procedure is used to determine whether or not the state-transition graph satisfies the specifications.We describe the basic model checking algorithm and show how it can be used with binary decision diagrams to verify properties of large state-transition graphs. We illustrate the power of model checking to find subtle errors by verifying part of theContingency Guidance Requirementsfor the Space Shuttle.