| 用于克服程序状态空间爆炸的条件化预处理 |
| |
| 引用本文： | 肖健宇,张德运,陈海诠,董皓. 用于克服程序状态空间爆炸的条件化预处理[J]. 计算机工程, 2006, 32(19): 51-53 |
| |
| 作者姓名： | 肖健宇 张德运 陈海诠 董皓 |
| |
| 作者单位： | 1. 湖南涉外经济学院计算机系,长沙,410205;西安交通大学电子与信息工程学院,西安,710049
2. 西安交通大学电子与信息工程学院,西安,710049 |
| |
| 摘 要： | 提出用条件化技术对程序进行预处理的方案，以克服软件模型检测中状态空间爆炸问题。以程序性质公式中蕴涵式的前件作为约束条件，通过对程序符号化执行后各控制点的路径条件进行逻辑推理，删除那些对性质检测无关的语句。理论分析和实验结果表明，条件化可以有效缩减程序状态空间，并且满足软件模型检测对状态缩减的安全性要求。
|
| 关 键 词： | 软件模型检测 状态-迁移模型 状态爆炸 程序条件化 自动定理证明 |
| 文章编号： | 1000-3428（2006）19-0051-03 |
| 收稿时间： | 2005-11-03 |
| 修稿时间： | 2005-11-03 |
Program Conditioning to Reduce State Space Explosion for Software Model Check |
| |
| XIAO Jianyu,ZHANG Deyun,CHEN Haiquan,DONG Hao. Program Conditioning to Reduce State Space Explosion for Software Model Check[J]. Computer Engineering, 2006, 32(19): 51-53 |
| |
| Authors: | XIAO Jianyu ZHANG Deyun CHEN Haiquan DONG Hao |
| |
| Affiliation: | (1. Dept. of Computer, Hunan International Economics University, Changsha 410205; 2. School of Electronics and Information Engineering, Xi’an Jiaotong University, Xi’an 710049) |
| |
| Abstract: | A scheme of applying technique of conditioning to preprocess a program is proposed to alleviate the problem of state space explosion faced by software model checking. It takes the antecedent of an implication form in linear temporal logic formula of program properties as the condition of program conditioning, reasons the path condition of each control point of the program after symbolic execution, and deletes the irrelevant statements with respect to the verification of the program properties. Theoretical analysis and experiments show that the scheme can effectively reduce a program’s state space and satisfy the safety requirement imposed by software model check. |
| |
| Keywords: | Software model check State-transition model State explosion Program conditioning Theorem proving |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载免费的PDF全文 |
