Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
复制标题
DOI：
10.1007/s00165-019-00483-2
复制
发表时间：
2019-05
影响因子：
1
通讯作者：
P. Antonino;Thomas Gibson-Robinson;A. W. Roscoe
中科院分区：
文献类型：
--
作者：
P. Antonino;Thomas Gibson-Robinson;A. W. Roscoe
这项工作开发了一种可以证明并发系统无死锁的本地分析类型。与检查系统的整体行为相反，局部分析包括检查系统小部分的行为以产生给定的属性。我们分析了相互作用的组件对来近似系统可达性，并提出了一个新的健全但不完整/近似的框架来检查死锁和局部死锁自由。通过用这个近似值替换精确可达性，它寻找死锁（或局部死锁）候选对象，即位于我们近似值内的阻塞（局部阻塞）系统状态。这种表征提高了当前近似技术的精度。特别是，它可以处理非遗传的无死锁系统，即具有死锁子系统的无死锁系统。这些是大多数近似技术所忽略的。此外，我们还演示了如何使用SAT检查器来有效地实现我们的框架，该框架通常比当前的死锁自由分析技术具有更好的伸缩性。通过一系列的实际实验证明了这一点。
This work develops a type of local analysis that can prove concurrent systems deadlock free. As opposed to examining the overall behaviour of a system, local analysis consists of examining the behaviour of small parts of the system to yield a given property. We analyse pairs of interacting components to approximate system reachability and propose a new sound but incomplete/approximate framework that checks deadlock and local-deadlock freedom. By replacing exact reachability by this approximation, it looks for deadlock (or local-deadlock) candidates, namely, blocked (locally-blocked) system states that lie within our approximation. This characterisation improves on the precision of current approximate techniques. In particular, it can tackle non-hereditary deadlock-free systems, namely, deadlock-free systems that have a deadlocking subsystem. These are neglected by most approximate techniques. Furthermore, we demonstrate how SAT checkers can be used to efficiently implement our framework, which, typically, scales better than current techniques for deadlock-freedom analysis. This is demonstrated by a series of practical experiments.