并行软件模型检测

• 作者: 罗贵明 邝宏斌
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 并行模型检测 软件模型检测 标号迁移系统 模块化验证
• 年，卷（期）: 2008,（19）
• 所属期刊栏目: 软件技术与数据库
• 页码范围: 23-25,29
• 页数: 4页
• 分类号: TP311.5
• 字数: 3563字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2008.19.009

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗贵明	清华大学信息科学与技术国家实验室	19	125	6.0	10.0
5	邝宏斌	清华大学信息科学与技术国家实验室	1	9	1.0	1.0