文件名称：程序重构预处理在提高软件模型检测效率中的应用
文件大小：351KB
文件格式：PDF
更新时间：2014-04-18 07:54:11
软件模型检测，谓词抽象，程序重构，状态爆炸，过程总结
针对软件模型检测目前很难处理大型程序的问题,提出用程序重构技术对待检的源代码进行预处理,以提高模型检测算法的效率.程序重构将大型程序分解成语义一致的小型过程的集合,由于模型检测算法中过程总结边可单独计算,而且在程序中对某过程的调用可能有多次,这种预处理可以避免状态空间的重复搜索,从而降低模型检测算法在空间和时间上的开销.根据表达程序性质的线性时序逻辑LTL公式的构成,给出了程序重构预处理前后程序语义相等的充分条件;并给定程序和性质公式,用blast作为程序模型检测实验工具,比较程序重构预处理前后blast的运行结果.理论分析和部分程序上的实验表明:程序重构预处理能降低大型程序的模型检测开销,并满足软件模型检测的安全性要求.