程序重构预处理在提高软件模型检测效率中的应用  

Program Restructuring to Improve Efficiency of Software Model Checking

作　　者：黄卫平[1] 

机构地区：[1]邵阳学院信息工程系

出　　处：《计算机研究与发展》2008年第8期1417-1422,共6页Journal of Computer Research and Development

基　　金：湖南省科技厅科技计划基金项目(2007JT2006);湖南省教育厅科技资助项目(06b011)~~

摘　　要：针对软件模型检测目前很难处理大型程序的问题,提出用程序重构技术对待检的源代码进行预处理,以提高模型检测算法的效率.程序重构将大型程序分解成语义一致的小型过程的集合,由于模型检测算法中过程总结边可单独计算,而且在程序中对某过程的调用可能有多次,这种预处理可以避免状态空间的重复搜索,从而降低模型检测算法在空间和时间上的开销.根据表达程序性质的线性时序逻辑LTL公式的构成,给出了程序重构预处理前后程序语义相等的充分条件;并给定程序和性质公式,用blast作为程序模型检测实验工具,比较程序重构预处理前后blast的运行结果.理论分析和部分程序上的实验表明:程序重构预处理能降低大型程序的模型检测开销,并满足软件模型检测的安全性要求.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 algorithm, and a procedure may be called many times in a program, the pre-processing can avoid unnecessary repetition of state space search so as to decrease the overhead of space and the time in model checking algorithm. According to the components of linear temporal logic, the sufficient conditions for semantical equality of program restructuring are given. Given programs and programs＇ property, the experimental results before and after restructuring the programs on the model checker ＂blast＂ are compared. Theoretical analysis and experimental results on some benchmark programs show that program restructuring can effectively decrease the overhead of model checking of large-scale programs, and at the same time, it can satisfy the security requirements of software model checking.

关 键 词：软件模型检测 谓词抽象 程序重构 状态爆炸 过程总结 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]