过程提取用于改善程序模型检测的可伸缩性
肖健宇1,2,张德运1,郑卫斌1
(1.西安交通大学电子与信息工程学院，710049,西安；2.邵阳学院激光与信息研究所，422000,湖南邵阳）
摘要:针对目前基于谓词抽象的程序模型检测工具很难处理大规模软件的现状，提出用过程提取技术对待检的源代码进行预处理，以改善程序模型检测的可伸缩性.首先，将程序中一个选定的语句集合提取出来并包装成一个独立的过程，然后在原程序的相应位置用一个过程调用替代，进而将大型程序分解成语义一致的小型过程的集合.由于模型检测算法中的过程总结边可单独计算，所以过程提取使整个程序的模型检测任务模块化，当程序对某过程进行多次调用时，利用总结边可以避免对过程体内状态空间的重复搜索，从而降低了模型检测算法在空间和时间上的开销.理论分析和实验表明，所提技术能有效缩短大型程序的模型检测时间，并在程序的转换中不会改变原程序语义，满足了程序模型检测的安全性要求.
关键词:程序模型检测；过程提取；任务模块化
中图分类号:TP311.1文献标识码:A文章编号:0253-987X(2006)06-0630-04