Integer Linear Programming-Based Property Checking for Asynchronous Reactive Systems
Integer Linear Programming-Based Property Checking for Asynchronous Reactive Systems
复制标题
DOI：
10.1109/tse.2011.1
复制
发表时间：
2013-02
影响因子：
7.4
通讯作者：
S. Leue;Wei Wei-Wei
中科院分区：
文献类型：
--
作者：
S. Leue;Wei Wei-Wei
异步反应式系统形成了广泛的软件系统的基础，例如在电信领域。严格地证明这些系统是正确设计的是非常可取的。然而，传统的形式化方法来验证这些系统往往是困难的，因为异步反应系统通常拥有非常大的，甚至无限的状态空间。我们提出了一个整数线性规划（ILP）求解为基础的属性检查框架，集中在局部分析的循环行为的每个单独的组成部分的系统。我们应用我们的框架检查的缓冲区有界性和活锁自由属性，这两者都是不可判定的异步反应系统具有无限的状态空间。我们说明了所提出的检查方法的应用程序Promela，SPIN模型检查器的输入语言。虽然我们的框架的精度仍然是一个问题，我们提出了一个反例指导的抽象细化过程的基础上发现的依赖控制流循环。我们已经实现了原型工具，我们在现实生活中的系统模型上获得了有希望的实验结果。
Asynchronous reactive systems form the basis of a wide range of software systems, for instance in the telecommunications domain. It is highly desirable to rigorously show that these systems are correctly designed. However, traditional formal approaches to the verification of these systems are often difficult because asynchronous reactive systems usually possess extremely large or even infinite state spaces. We propose an integer linear program (ILP) solving-based property checking framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. We apply our framework to the checking of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space. We illustrate the application of the proposed checking methods to Promela, the input language of the SPIN model checker. While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependences among control flow cycles. We have implemented prototype tools with which we obtained promising experimental results on real-life system models.