论文标题
局部国家空间分析以减少部分订单
Local State Space Analysis to Assist Partial Order Reduction
论文作者
论文摘要
本文提出了一种用于模型检查并发系统更有效的部分订单的方法。这种方法利用构图可及性分析来为并发系统中的所有过程生成过度陈列的局部状态过渡模型，在该系统中可以提取独立关系和其他有用的信息。与通过静态分析系统描述获得的独立关系相比，提取的独立关系更精确和完善，因此会导致更有效的部分级阶降低。在一组并发系统示例中证明了这种方法。与使用自旋获得的情况相比，在几种情况下，已经观察到状态空间的降低明显更高。
This paper presents an approach to more efficient partial order reduction for model checking concurrent systems. This approach utilizes a compositional reachability analysis to generate over-approximate local state transition models for all processes in a concurrent system where an independence relation and other useful information can be extracted. The extracted independence relation, compared to what can be obtained by statically analyzing the system descriptions, is more precise and refined, therefore leads to more efficient partial order reduction. This approach is demonstrated on a set of concurrent system examples. Significantly higher reduction in state space has been observed in several cases compared to what can be obtained using SPIN.
