| 并行软件模型检测 |
| |
| 引用本文： | 邝宏斌,罗贵明. 并行软件模型检测[J]. 计算机工程, 2008, 34(19): 23-25,2 |
| |
| 作者姓名： | 邝宏斌 罗贵明 |
| |
| 作者单位： | 清华大学信息科学与技术国家实验室,北京,100084;清华大学软件学院,北京,100084 |
| |
| 基金项目： | 国家自然科学基金，清华大学校科研和教改项目 |
| |
| 摘 要： | 并行化是提高模型检测效率的重要手段。该文研究了基于标号迁移系统的C程序模型检测，提出一种软件模型检测并行化的方法。该方法利用软件模型检测工具模块化验证(MAGIC)的模块化特性对C程序进行组件分解，将各组件均衡地分发到若干计算节点，由节点调用MAGIC完成验证。由于保证节点间只有少量的通信与同步，该方法能达到较好的并行加速比，具有良好的可扩展性。实验结果显示，该方法大幅压缩了检测时间，有利于大规模软件的形式化验证。
|
| 关 键 词： | 并行模型检测 软件模型检测 标号迁移系统 模块化验证 |
| 修稿时间： | |
Parallel Software Model Checking |
| |
| KUANG Hong-bin,LUO Gui-ming. Parallel Software Model Checking[J]. Computer Engineering, 2008, 34(19): 23-25,2 |
| |
| Authors: | KUANG Hong-bin LUO Gui-ming |
| |
| Affiliation: | (1. National Laboratory for Information Science and Technology, Tsinghua University, Beijing 100084; 2. School of Software, Tsinghua University, Beijing 100084) |
| |
| 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. |
| |
| Keywords: | parallel model checking software model checking Labeled Transition Systems(LTS) MAGIC |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载免费的PDF全文 |
