程序模型检测的两阶段框架  

Two-phase framework of program model checking

作　　者：缪力[1] 张大方[1] 

机构地区：[1]湖南大学软件学院,长沙410082

出　　处：《计算机应用》2007年第12期3089-3091,共3页journal of Computer Applications

基　　金：国家自然科学基金资助项目(60673155)

摘　　要：模型检测是一种对有限状态变迁系统验证其时态逻辑性质的重要方法,可以弥补测试技术的不足。基于流分析的程序模型检测和基于语言转换的程序模型检测是当前程序模型检测的主要方法,它们都存在各自的局限性。基于对这两种程序模型检测方法各自优缺点的分析,提出了一种两阶段程序模型检测框架,通过结合两种程序模型检测方法,可有效提高程序模型检测对较大规模程序的适用性。Model checking is an important method of verifying logic properties of finite state systems, and also a supplement to the shortage of software testing. Flow analysis and language transform are two main methods for program model checking, but both are limited in practice. Based on the analysis of shortages and strong points of two program model checking methods, a two-phase program model checking framework was proposed, which can efficiently improve the applicability of checking large programs with the framework by integrating two methods of program model checking.

关 键 词：程序模型检测 流分析 SPIN 程序分析 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]