Efficient Verification of Concurrent Systems Using Synchronisation Analysis and SAT/SMT Solving
Efficient Verification of Concurrent Systems Using Synchronisation Analysis and SAT/SMT Solving
复制标题
DOI：
10.1145/3335149
复制
发表时间：
2019-07
期刊：
影响因子：
--
通讯作者：
P. Antonino;Thomas Gibson-Robinson;A. W. Roscoe
中科院分区：
文献类型：
--
作者：
P. Antonino;Thomas Gibson-Robinson;A. W. Roscoe
本文研究了如何使用近似可以使并发系统的形式化验证可扩展。我们提出了同步分析的思想，自动捕获全局不变量和近似可达性。我们计算组件如何参与全球系统同步的不变量，并使用这些不变量之间的一致性的概念，以建立组件是否可以有效地通信，以达到一些系统状态。我们的同步分析技术试图表明，无论是一个系统状态是不可达的，通过演示组件不能同意他们参与系统规则的顺序，或系统状态是不可达的，通过演示组件不能同意他们参与系统规则的次数。这些全自动的技术被应用于检查死锁和局部死锁自由的PairStatic框架。它扩展了对（最近的一个框架，我们使用纯成对分析组件和SAT检查器来检查死锁和本地死锁自由）与技术进行同步分析。因此，它不仅可以计算与Pair相同的局部不变量，还可以利用同步分析发现的全局不变量，从而提高可达性近似并加强我们的验证。我们使用SAT/SMT在DeadlOx工具中实现PairStatic，并展示了它们在检查（本地）死锁自由度方面的改进。
This article investigates how the use of approximations can make the formal verification of concurrent systems scalable. We propose the idea of synchronisation analysis to automatically capture global invariants and approximate reachability. We calculate invariants on how components participate on global system synchronisations and use a notion of consistency between these invariants to establish whether components can effectively communicate to reach some system state. Our synchronisation-analysis techniques try to show either that a system state is unreachable by demonstrating that components cannot agree on the order they participate in system rules or that a system state is unreachable by demonstrating components cannot agree on the number of times they participate on system rules. These fully automatic techniques are applied to check deadlock and local-deadlock freedom in the PairStatic framework. It extends Pair (a recent framework where we use pure pairwise analysis of components and SAT checkers to check deadlock and local-deadlock freedom) with techniques to carry out synchronisation analysis. So, not only can it compute the same local invariants that Pair does, it can leverage global invariants found by synchronisation analysis, thereby improving the reachability approximation and tightening our verifications. We implement PairStatic in our DeadlOx tool using SAT/SMT and demonstrate the improvements they create in checking (local) deadlock freedom.