Assume-Guarantee Model Checking of Software: A Comparative Case Study
Assume-Guarantee Model Checking of Software: A Comparative Case Study
复制标题
软件的假设保证模型检查：比较案例研究
作者：
C. Păsăreanu;Matthew B. Dwyer;M. Huth
文献中已经提出了各种假设模型检查方法。在本文中，我们描述了使用旋转和SMV模型检查器检查软件组件（单元）的这些方法的几种可能实现。一般而言，模型检查软件单元需要建立单元执行的运行时上下文的环境的定义。我们描述了如何从LTL中编写的假定环境行为的规范中综合此类环境的实现。然后，这些环境可用于检查软件单元必须保证可以用LTL或ACTL编写的属性。我们报告了几项实验，这些实验提供了有关不同假设保证方法相对性能的证据。
A variety of assume-guarantee model checking approaches have been proposed in the literature. In this paper, we describe several possible implementations of those approaches for checking properties of software components (units) using SPIN and SMV model checkers. Model checking software units requires, in general, the definition of an environment which establishes the run-time context in which the unit executes. We describe how implementations of such environments can be synthesized from specifications of assumed environment behavior written in LTL. Those environments can then be used to check properties that the software unit must guarantee which can be written in LTL or ACTL. We report on several experiments that provide evidence about the relative performance of the different assume-guarantee approaches.