Concrete Model Checking with Abstract Matching and Refinement
Concrete Model Checking with Abstract Matching and Refinement
复制标题
通过抽象匹配和细化进行具体模型检查
DOI：
10.1007/11513988_7
复制
发表时间：
2005
影响因子：
--
通讯作者：
W. Visser
中科院分区：
文献类型：
--
作者：
C. Păsăreanu;Radek Pelánek;W. Visser
我们提出了一种基于抽象的模型检测方法，该方法依赖于对被分析系统的可行行为的下近似的精化。该方法保留了对安全属性的错误，因为根据定义，所有分析的行为都是可行的。该方法不需要生成抽象转换关系，而是在存储由一组抽象谓词指定的具体状态的抽象版本的同时执行具体转换。对于每个探索的转换，该方法在定理证明器的帮助下检查是否存在任何由抽象引入的精度损失。这些检查的结果用于决定终止或通过生成新的抽象谓词来改进抽象。如果被分析的(可能是无限的)混凝土系统有一个有限互拟合商，则该方法保证最终得到一个等价的有限双相似结构。我们举例说明了该方法在并发程序检测中的应用。我们还展示了如何使用轻量级变体进行有效的软件测试。
We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while storing abstract versions of the concrete states, as specified by a set of abstraction predicates. For each explored transition the method checks, with the help of a theorem prover, whether there is any loss of precision introduced by abstraction. The results of these checks are used to decide termination or to refine the abstraction by generating new abstraction predicates. If the (possibly infinite) concrete system under analysis has a finite bisimulation quotient, then the method is guaranteed to eventually explore an equivalent finite bisimilar structure. We illustrate the application of the approach for checking concurrent programs. We also show how a lightweight variant can be used for efficient software testing.