SAT-Based Bounded Strong Satisfiability Checking of Reactive System Specifications
SAT-Based Bounded Strong Satisfiability Checking of Reactive System Specifications
复制标题
基于 SAT 的反应式系统规范有界强可满足性检查
DOI：
10.1007/978-3-642-36818-9_7
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Naoki Yonezaki
中科院分区：
文献类型：
--
作者：
Masaya Shimakawa;Shigeki Hagihara;Naoki Yonezaki
许多涉及安全关键反应系统的致命事故都发生在系统设计和测试阶段未考虑的意外情况下。为了防止这些事故，反应式系统应该设计成在任何时候都能对来自环境的任何请求做出适当的响应。在规范阶段验证此属性可以减少开发返工。规格说明的这种性质通常称为可实现性。反应式系统规范的可实现性检查涉及复杂和错综复杂的分析。为了检测规格说明中的简单和典型缺陷，我们引入了有界强可满足性（可实现性的必要条件）的概念，并给出了检查此属性的方法。有界强可满足性是这样一种性质，即对于给定sizek的循环结构所表示的所有输入模式，存在满足给定规范的响应。我们提出了一个检查方法的基础上的可满足性求解器，并报告实验结果。
Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations that were not considered during the design and test phases of the systems. To prevent these accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces development reworking. This property of a specification is commonly known as realizability. Realizability checking for reactive system specifications involves complex and intricate analysis. For the purpose of detecting simple and typical defects in specifications, we introduce the notion of bounded strong satisfiability (a necessary condition for realizability), and present a method for checking this property. Bounded strong satisfiability is the property that for all input patterns represented by loop structures of a given sizek, there is a response that satisfies a given specification. We present a checking method based on a satisfiability solver, and report experimental results.