作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2009, Vol. 35 ›› Issue (19): 65-68. doi: 10.3969/j.issn.1000-3428.2009.19.021

• 软件技术与数据库 • 上一篇    下一篇

基于CEGAR偏序化简的并行程序死锁检测

梁中兴,罗贵明,旷宏斌   

  1. (清华大学软件学院,北京 100084)
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2009-10-05 发布日期:2009-10-05

On-the-fly Deadlock Detection with Partial-order Reduction Based on CEGAR

LIANG Zhong-xing, LUO Gui-ming, KUANG Hong-bin   

  1. (School of Software, Tsinghua University, Beijing 100084)
  • Received:1900-01-01 Revised:1900-01-01 Online:2009-10-05 Published:2009-10-05

摘要: 针对并发程序的模型检测存在大量的冗余交互和严重的状态空间爆炸问题,提出以迁移标记系统为建模语言计算Persistent Set并完成偏序化简的算法。将算法和CEGAR算法结合起来,实现对并发C程序的并行死锁检测。结果证明该算法在减缓状态空间爆炸和模型验证的效率方面较以往的算法有所提高。

关键词: 模型检测, CEGAR算法, 偏序化简

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

中图分类号: