并行软件模型检测

摘要：

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

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

所属期刊栏目：34

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金资助项60474026,60672110;清华大学研究基金;清华大学信息学院基金

在线出版日期：2008-12-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：23-25,29