Parameterized verification through view abstraction
Parameterized verification through view abstraction
复制标题
DOI：
10.1007/s10009-015-0406-x
复制
发表时间：
2016-10-01
影响因子：
1.5
通讯作者：
Holik, Lukas
中科院分区：
文献类型：
--
作者：
Abdulla, Parosh;Haziza, Frederic;Holik, Lukas
我们提出了一个简单而有效的框架，用于自动验证具有参数数量的通信进程的系统。这些过程可以以各种拓扑来组织，例如字、多重集、环或树。我们的方法只需要检查少量进程即可显示整个系统的正确性。它依赖于一个抽象函数，该函数从固定数量的进程的角度来看待系统。在验证过程中使用抽象来动态检测分界点，超过该分界点就不需要继续状态空间的搜索。我们证明该方法对于包括 Petri 网在内的一大类准有序系统来说是完整的。我们对各种基准测试的实验表明，该方法非常高效，即使对于具有不可判定验证问题的系统类别也能很好地工作。特别是，该方法处理细粒度和完整版本的 Szymanski 互斥协议，据我们所知，其正确性尚未被任何其他现有方法自动证明。
We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.