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

• 作者: 黄卫平
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 软件模型检测 谓词抽象 程序重构 状态爆炸 过程总结
• 年，卷（期）: 2008,（8）
• 所属期刊栏目: 软件技术
• 页码范围: 1417-1422
• 页数: 6页
• 分类号: TP311.1
• 字数: 5260字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄卫平	邵阳学院信息工程系	2	12	1.0	2.0