| 程序重构预处理在提高软件模型检测效率中的应用 |
| |
| 引用本文： | 黄卫平.程序重构预处理在提高软件模型检测效率中的应用[J].计算机研究与发展,2008,45(8). |
| |
| 作者姓名： | 黄卫平 |
| |
| 作者单位： | 邵阳学院信息工程系,湖南邵阳,422000;武汉大学国际软件学院,武汉,430072 |
| |
| 基金项目： | 湖南省科技厅科技攻关项目，湖南省教育厅科研项目 |
| |
| 摘 要： | 针对软件模型检测目前很难处理大型程序的问题,提出用程序重构技术对待检的源代码进行预处理,以提高模型检测算法的效率.程序重构将大型程序分解成语义一致的小型过程的集合,由于模型检测算法中过程总结边可单独计算,而且在程序中对某过程的调用可能有多次,这种预处理可以避免状态空间的重复搜索,从而降低模型检测算法在空间和时间上的开销.根据表达程序性质的线性时序逻辑LTL公式的构成,给出了程序重构预处理前后程序语义相等的充分条件;并给定程序和性质公式,用blast作为程序模型检测实验工具,比较程序重构预处理前后blast的运行结果.理论分析和部分程序上的实验表明:程序重构预处理能降低大型程序的模型检测开销,并满足软件模型检测的安全性要求.
|
| 关 键 词： | 软件模型检测 谓词抽象 程序重构 状态爆炸 过程总结 |
Program Restructuring to Improve Efficiency of Software Model Checking |
| |
| Huang Weiping.Program Restructuring to Improve Efficiency of Software Model Checking[J].Journal of Computer Research and Development,2008,45(8). |
| |
| Authors: | Huang Weiping |
| |
| Affiliation: | Huang Weiping(Department of Information Engineering,Shaoyang University,Shaoyang,Hunan 422000)(International School of Software,Wuhan University,Wuhan 430072) |
| |
| Abstract: | In order to cope with the problem,that is,the currently available software model checker can hardly deal with large-scale software,it is proposed to use the technique of program restructuring to pre-process the source code,so as to enhance the efficiency of software model checking.Program restructuring decomposes a large-scale program into a set of small procedures which preserves the original semantics.Due to the fact that the procedure summary edge can be separately computed in the model-checking algorith... |
| |
| Keywords: | software model checking predicate abstraction program restructuring state explosion procedure summary |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
