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

计算机工程 ›› 2008, Vol. 34 ›› Issue (19): 23-25,2. doi: 10.3969/j.issn.1000-3428.2008.19.009

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

并行软件模型检测

邝宏斌1,2,罗贵明1,2   

  1. (1. 清华大学信息科学与技术国家实验室,北京 100084;2. 清华大学软件学院,北京 100084)
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-10-05 发布日期:2008-10-05

Parallel Software Model Checking

KUANG Hong-bin1,2, LUO Gui-ming1,2   

  1. (1. National Laboratory for Information Science and Technology, Tsinghua University, Beijing 100084; 2. School of Software, Tsinghua University, Beijing 100084)
  • Received:1900-01-01 Revised:1900-01-01 Online:2008-10-05 Published:2008-10-05

摘要: 并行化是提高模型检测效率的重要手段。该文研究了基于标号迁移系统的C程序模型检测,提出一种软件模型检测并行化的方法。该方法利用软件模型检测工具模块化验证(MAGIC)的模块化特性对C程序进行组件分解,将各组件均衡地分发到若干计算节点,由节点调用MAGIC完成验证。由于保证节点间只有少量的通信与同步,该方法能达到较好的并行加速比,具有良好的可扩展性。实验结果显示,该方法大幅压缩了检测时间,有利于大规模软件的形式化验证。

关键词: 并行模型检测, 软件模型检测, 标号迁移系统, 模块化验证

Abstract: Parallelism is an effective method in improving the efficiency of model checking. C program model checking based on LTS is studied and a methodology for parallel software model checking is presented. It utilizes modularity of MAGIC, a software model checker, to decompose C program into components, distributes them over computational nodes and parallel call MAGIC to complete the verification. Close to linear speedup and good scalability can be achieved due to little synchronization and inter-nodes communication. The reduction of time expense is beneficial to formal verification of large-scale software.

Key words: parallel model checking, software model checking, Labeled Transition Systems(LTS), MAGIC

中图分类号: