A comparative study between linear programming verification (LPV) and other verification methods
A comparative study between linear programming verification (LPV) and other verification methods
复制标题
线性规划验证（LPV）与其他验证方法的比较研究
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
J. Lambert
中科院分区：
文献类型：
--
作者：
Samuel Devulder;J. Lambert
比较我们的线性规划技术的软件验证（LPV）与其他验证系统：显式探索使用偏序约简（自旋）和隐式探索使用BDD（Xeve/Esterel）。案例研究是一个容易扩展的问题（总线仲裁器）的安全属性。结果表明，基于探索的方法（自旋和Xeve/Esterel）具有整体指数复杂性，限制了它们在小实例上的使用。LPV技术不依赖于探索，是唯一一种足够快（二次复杂度）的技术，可以处理比本文中提出的其他技术大50倍的系统。此外，与基于探索的方法相反，LPV产生真实的已证明的事实，这意味着这种技术与定理证明有一些共同点。我们相信，LPV的尺度变化的鲁棒性表明，线性规划可以成功地应用于工业系统的验证。
Compares our linear programming technology for software verification (LPV) with other verification systems: explicit exploration using partial order reduction (Spin) and implicit exploration using BDDs (Xeve/Esterel). The case study is a safety property of an easily-scalable problem (a bus arbiter). The results show that exploration-based methods (Spin and Xeve/Esterel) have an overall exponential complexity, restricting their use on small instances. The LPV technique, which does not rely on exploration, is the only one fast enough (quadratic complexity) to handle systems that are 50 times larger than the other techniques presented in this paper can do. Moreover, in opposition to exploration-based methods, LPV produces real proven facts that mean this technique shares some common points with theorem proving. We believe that the scale-change robustness of LPV shows that linear programming can be applied successfully to the verification of industrial systems.