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