Software Verification Based on Linear Programming
Software Verification Based on Linear Programming
复制标题
基于线性规划的软件验证
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
J. Lambert
中科院分区：
文献类型：
--
作者：
S. Dellacherie;Samuel Devulder;J. Lambert
本文提出了一种新的基于普通线性规划的软件验证方法。问题是给定一个软件S和一个属性P，以确定是否存在S满足P的路径（即测试序列），或者P不可能满足的证明。
软件S被建模为一组通信自动机，这反过来又被转化为一个系统的线性方程组的正数。性质P然后被转换为添加到该系统的额外线性方程。
我们定义的扩展概念的流路径（其中包括路径的概念），允许自动机进行数据流，而不是不可分割的令牌。通过将线性规划以复杂的方式应用于线性系统，可以在大小为（S;P）的时间多项式中显示S满足P的流路或证明P不可能满足。
流路径的存在并不总是意味着路径的存在，因为它可以是非整数值。然而，在我们所有的模型化例子中，对流路解的研究总是允许显示满足P的路径，或者强调证明P不可能满足的理由。
本文的第一部分介绍了我们的方法的理论背景。第二部分总结了我们的方法在一些工业规模的系统上的应用结果。
We introduce a new software verification method based on plain linear programming. The problematic is being given a software S and a property P, to find whether there exists a path (i.e. a test sequence) of S satisfying P, or a proof that P is impossible to satisfy.
The software S is modelized as a set of communicating automata which in turn is translated into a system of linear equations in positive numbers. Property P is then translated as extra linear equations added to this system.
We define the extended notion of flow-path (which includes the notion of path) permitting the automata to carry flows of data rather than undividable tokens. By applying linear programming in a sophisticated way to the linear system, it is possible, in time polynomial in the size of (S;P), either to display a flow-path of S satisfying P or to prove that P is impossible to satisfy.
The existence of a flow-path does not always imply the existence of a path, as it can be non-integer valued. Yet, on all our modelized examples, the study of the flow-path solution always permitted either to display a path satisfying P or to underscore a reason proving P to be impossible to satisfy.
The first part of this document introduces the theoretical background of our method. The second part sums up results of the use of our method on some systems of industrial size.