论文标题
基于模式的僵持自由分析策略并发系统
A Pattern-based deadlock-freedom analysis strategy for concurrent systems
论文作者
论文摘要
长期以来，本地分析被认为是解决状态空间爆炸问题的有效工具。在这项工作中，我们提出了一种将局部分析在验证并发和分布式系统验证僵局自由时系统化的方法。它结合了系统分解的策略和通过遵守行为模式对分解子系统的验证。从工作的核心中，我们有许多CSP改进表达式，使我们的方法的用户可以自动验证我们施加的所有行为限制。我们还提出了一个原型工具来支持我们的方法。最后，我们通过分析将其应用于某些示例时的票价来证明我们的方法可以产生的实际影响。
Local analysis has long been recognised as an effective tool to combat the state-space explosion problem. In this work, we propose a method that systematises the use of local analysis in the verification of deadlock freedom for concurrent and distributed systems. It combines a strategy for system decomposition with the verification of the decomposed subsystems via adherence to behavioural patterns. At the core of our work, we have a number of CSP refinement expressions that allows the user of our method to automatically verify all the behavioural restrictions that we impose. We also propose a prototype tool to support our method. Finally, we demonstrate the practical impact our method can have by analysing how it fares when applied to some examples.
