Abstract:
In model checking of concurrent programs, the redundant parallel composition and combinatorial state explosion are the crucial issues. This paper presents a novel approach to compute the persistent sets for partial-order reduction of labeled transition systems. The method is incorporated in Counterexample-Guided Abstraction Refinement(CEGAR) frame for on-the-fly deadlock detection in C program. The results prove that the algorithm slowdowns the state space explosion and has a significant improvement in efficiency compared with the algorithms used before.
Key words:
model cheking,
Counterexample-Guided Abstraction Refinement(CEGAR) algorithm,
partial-order reduction
摘要： 针对并发程序的模型检测存在大量的冗余交互和严重的状态空间爆炸问题，提出以迁移标记系统为建模语言计算Persistent Set并完成偏序化简的算法。将算法和CEGAR算法结合起来，实现对并发C程序的并行死锁检测。结果证明该算法在减缓状态空间爆炸和模型验证的效率方面较以往的算法有所提高。
关键词:
模型检测,
CEGAR算法,
偏序化简
CLC Number:
LIANG Zhong-xing; LUO Gui-ming; KUANG Hong-bin. On-the-fly Deadlock Detection with Partial-order Reduction Based on CEGAR[J]. Computer Engineering, 2009, 35(19): 65-68.
梁中兴;罗贵明;旷宏斌. 基于CEGAR偏序化简的并行程序死锁检测[J]. 计算机工程, 2009, 35(19): 65-68.