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

• 作者: 张涛 彭飞 王金双 赵敏
• 来源期刊: 军事通信技术
• 学科: 工学
• 关键词: 形式化方法 形式化验证 模型检测 状态爆炸
• 年，卷（期）: 2016,（2）
• 所属期刊栏目: 综述与评论
• 页码范围: 38-42,76
• 页数: 6页
• 分类号: TP391.41
• 语种: 中文
• DOI: 10.16464/j.cnki.cn32-1289.2016.02.008

摘要

随着计算机系统的功能日益强大,对其进行功能和正确性测试与验证的复杂度也越来越大.形式化方法作为对计算机系统进行描述与验证的重要途径,得到学术界普遍的关注与认可.文章主要介绍形式化方法,详细介绍模型检测的检测原理及其主要技术,介绍了几种典型的模型检测工具,并对它们的性能进行比较,同时研究了模型检测中普遍存在的状态爆炸问题及缩减状态方法,最后介绍模型检测的新进展.文章可为模型检测方法研究提供参考和理论支撑.