过程提取用于改善程序模型检测的可伸缩性

• 作者: 张德运 肖健宇 郑卫斌
• 来源期刊: 西安交通大学学报
• 关键词: 程序模型检测 过程提取 任务模块化
• 年，卷（期）: 2006,（6）
• 所属期刊栏目: 专题研究
• 页码范围: 630-633
• 页数: 4页
• 分类号: TP311.1
• 语种: 中文
• DOI: 10.3321/j.issn:0253-987X.2006.06.003

摘要

针对目前基于谓词抽象的程序模型检测工具很难处理大规模软件的现状,提出用过程提取技术对待检的源代码进行预处理,以改善程序模型检测的可伸缩性.首先,将程序中一个选定的语句集合提取出来并包装成一个独立的过程,然后在原程序的相应位置用一个过程调用替代,进而将大型程序分解成语义一致的小型过程的集合.由于模型检测算法中的过程总结边可单独计算,所以过程提取使整个程序的模型检测任务模块化,当程序对某过程进行多次调用时,利用总结边可以避免对过程体内状态空间的重复搜索,从而降低了模型检测算法在空间和时间上的开销.理论分析和实验表明,所提技术能有效缩短大型程序的模型检测时间,并在程序的转换中不会改变原程序语义,满足了程序模型检测的安全性要求.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张德运	西安交通大学电子与信息工程学院	184	2190	23.0	37.0
2	郑卫斌	西安交通大学电子与信息工程学院	23	135	7.0	11.0
3	肖健宇	西安交通大学电子与信息工程学院	13	83	6.0	8.0