| 程序重构预处理在提高软件模型检测效率中的应用 |
| |
| 引用本文： | 黄卫平. 程序重构预处理在提高软件模型检测效率中的应用[J]. 计算机研究与发展, 2008, 45(8): 1417-1422. |
| |
| 作者姓名： | 黄卫平 |
| |
| 作者单位： | 1.(邵阳学院信息工程系 湖南邵阳 422000) (武汉大学国际软件学院 武汉 430072) (hwp0739@163.com) |
| |
| 基金项目： | 湖南省科技厅科技攻关项目,湖南省教育厅科研项目 |
| |
| 摘 要： | 针对软件模型检测目前很难处理大型程序的问题,提出用程序重构技术对待检的源代码进行预处理,以提高模型检测算法的效率.程序重构将大型程序分解成语义一致的小型过程的集合,由于模型检测算法中过程总结边可单独计算,而且在程序中对某过程的调用可能有多次,这种预处理可以避免状态空间的重复搜索,从而降低模型检测算法在空间和时间上的开销.根据表达程序性质的线性时序逻辑LTL公式的构成,给出了程序重构预处理前后程序语义相等的充分条件;并给定程序和性质公式,用blast作为程序模型检测实验工具,比较程序重构预处理前后blast的运行结果.理论分析和部分程序上的实验表明：程序重构预处理能降低大型程序的模型检测开销,并满足软件模型检测的安全性要求.
|
| 关 键 词： | 软件模型检测 谓词抽象 程序重构 状态爆炸 过程总结 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机研究与发展》浏览原始摘要信息 |
|
点击此处可从《计算机研究与发展》下载免费的PDF全文 |
|
