Cluster-Based Partial-Order Reduction
Cluster-Based Partial-Order Reduction
复制标题
基于簇的偏序约简
DOI：
10.1023/b:ause.0000038937.18006.3d
复制
发表时间：
2004
影响因子：
3.4
通讯作者：
M. Geilen
中科院分区：
文献类型：
--
作者：
T. Basten;D. Bosnacki;M. Geilen
通过穷举遍历状态空间来验证并发系统存在着臭名昭著的状态空间爆炸问题，这是由系统中不同进程的动作交织引起的。偏序降阶是解决这一问题的一种众所周知的技术。本文利用并发系统的层次化结构，对Holzmann和Pelded的偏序降阶方案进行了改进。我们的技术试图包含进程集群中动作之间的依赖关系，利用不同集群中动作的独立性来减少要验证的状态空间，同时保留感兴趣的属性。本文从部分降阶技术的形式化开始，接着介绍了我们的增强技术，包括正确性论证。新技术已在验证工具SPIN中实现。我们给出了实现细节、一些小实验和一个使用高速缓存一致性协议的大型案例研究。实验结果令人鼓舞。与标准的偏序约简相比，约简的状态数从21%提高到98%，状态转移数目从34%提高到99%。
The verification of concurrent systems through an exhaustive traversal of the state space suffers from the infamous state-space-explosion problem, caused by the many interleavings of actions of different processes in the system. Partial-order reduction is a well-known technique to tackle this problem. In this paper, we present an enhancement of the partial-order-reduction scheme of Holzmann and Peled that uses the hierarchical structure of concurrent systems. Our technique tries to contain dependencies between actions within clusters of processes, capitalizing on the independence of actions in different clusters to reduce the state space to be verified while preserving properties of interest. The paper starts with a formalization of the partial-order-reduction technique and continues with a presentation of our enhanced technique, including a correctness argument. The new technique has been implemented in the verification tool SPIN. We present implementation details, some small experiments, and one larger case study using a cache coherency protocol. The experimental results are encouraging. Compared to standard partial-order reduction, improvements in reductions are obtained from 21% up to 98% in the number of states and 34% up to 99% in the number of state transitions.