计算机系统形式化验证中的模型检测方法综述  

Overview of Model Checking Methods in Computer System Formal Verification

作　　者：彭飞[1] 张涛[2] 王金双[2] 赵敏[2] 

机构地区：[1]解放军理工大学指挥信息系统学院研究生1队,江苏南京210007 [2]解放军理工大学指挥信息系统学院

出　　处：《军事通信技术》2016年第2期38-42,76,共6页Journal of Military Communications Technology

摘　　要：随着计算机系统的功能日益强大,对其进行功能和正确性测试与验证的复杂度也越来越大。形式化方法作为对计算机系统进行描述与验证的重要途径,得到学术界普遍的关注与认可。文章主要介绍形式化方法,详细介绍模型检测的检测原理及其主要技术,介绍了几种典型的模型检测工具,并对它们的性能进行比较,同时研究了模型检测中普遍存在的状态爆炸问题及缩减状态方法,最后介绍模型检测的新进展。文章可为模型检测方法研究提供参考和理论支撑。As the functions of computer system become increasingly stronger, the testing and verifying of its function and correctness has become more complicated. Formal method is an im- portant way, which can describe and verify the computer system, and achieve more attention and recognition. The basic idea of formal method was introduced, and detail information about the detection principle and the main technology of model checking were presented. Several kinds of typical model checking tools were introduced and their performances compared. At the same time, the state explosion existing generally in model checking was studied and some strategies to reduce the amount of states put forward. Finally, some new achievement was discussed. The pa- per can provide reference and theoretical support for study of model checking method.

关 键 词：形式化方法 形式化验证 模型检测 状态爆炸 

分 类 号：TP391.41[自动化与计算机技术—计算机应用技术]