作　　者： ; ; ;

机构地区： 西安交通大学电子与信息工程学院

出　　处： 《西安交通大学学报》 2006年第6期630-633,共4页

摘　　要： 针对目前基于谓词抽象的程序模型检测工具很难处理大规模软件的现状,提出用过程提取技术对待检的源代码进行预处理,以改善程序模型检测的可伸缩性.首先,将程序中一个选定的语句集合提取出来并包装成一个独立的过程,然后在原程序的相应位置用一个过程调用替代,进而将大型程序分解成语义一致的小型过程的集合.由于模型检测算法中的过程总结边可单独计算,所以过程提取使整个程序的模型检测任务模块化,当程序对某过程进行多次调用时,利用总结边可以避免对过程体内状态空间的重复搜索,从而降低了模型检测算法在空间和时间上的开销.理论分析和实验表明,所提技术能有效缩短大型程序的模型检测时间,并在程序的转换中不会改变原程序语义,满足了程序模型检测的安全性要求. Aiming at the situation that the currently available program model checker cannot deal with large-scale software, the technique of procedure extraction was proposed to pre-process the source code in order to improve the scalability of software model checking. Firstly, a selected set of sentences （may be noncontiguous） is extracted and packaged as an independent procedure, and then the corresponding places that are in the original program are deleted and replaced by a proce- dure call, so as to decompose 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, the procedure extraction can modularize the task of program model checking. Since a procedure may be called many times in a program, unnecessary repetition of state space search in procedure bodies can be avoided by using summary edges so as to decrease the overhead of space and time in model checking algorithm. Theoretical analysis and experiment show that the technique of procedure extraction can effectively improve the sealability of model checking large-scale programs, and at the same time, it can preserve the semantics after transformations of the programs and satisfy the security requirements of software model checking.

关 键 词： 程序模型检测 过程提取 任务模块化

领　　域： [自动化与计算机技术] [自动化与计算机技术]