在航空航天、交通运输、核电能源和医疗卫生等安全苛求领域，系统的安全性尤为重要，为了确保系统安全，防止灾难性事故的发生，科技人员提出了诸多理论和方法，其中模型检测以其简洁明了和自动化程度高的优点而引人注目，其算法和应用研究成了学术界和工业界研究的热点话题之一。本书在讲解模型检测基础理论与基本方法的基础上，主要介绍笔者以广义Büchi自动机为研究对象，在模型检测算法及其安全性分析应用研究方面所取得的独创性研究成果，主要包括基于启发式NDFS的模型检测算法、基于启发式SCCs的广义Büchi自动机判空检测算法、基于启发式on-the-fly的扩展TGBA模型检测算法、基于场景分析的系统形式化模型生成方法、基于模型检测的系统安全性验证方法、基于故障注入的模型检测分析、铁路车站联锁系统的安全性分析研究。
本书可以作为计算机软件与理论、计算机应用、软件工程、自动化控制、信息安全、网络空间安全等专业类研究生课程教材，也可以作为相关领域科技人员的参考用书。

第1章 绪论
1.1 研究背景
1.2 国内外研究现状
1.2.1 模型检测相关研究
1.2.2 安全苛求系统的安全性研究现状
1.2.3 模型检测与安全性分析研究现状
1.3 研究内容
1.4 本书的结构安排
第2章 基于Büchi自动机的模型检测理论与方法
2.1 Büchi自动机基本原理
2.1.1 标准Büchi自动机
2.1.2 广义Büchi自动机
2.2 模型检测基本原理
2.2.1 系统建模
2.2.2 属性描述
2.2.3 模型验证
2.3 基于LTL的模型检测
2.4 基于Büchi自动机的模型检测方法
2.5 本章小结
第3章 基于启发式NDFS的模型检测算法
3.1 NDFS模型检测算法研究现状
3.2 基本概念及相关技术
3.2.1 TGBA简介
3.2.2 相关技术
3.3 HNDFS算法描述
3.4 HNDFS算法正确性证明
3.5 HNDFS算法复杂度分析
3.6 实验与分析
3.7 本章小结
第4章 基于启发式SCCs的广义Büchi自动机判空检测算法
4.1 引言
4.2 HSCCsEC算法描述
4.4 HSCCsEC算法实例
4.5 HSCCsEC算法正确性证明
4.6 HSCCsEC算法复杂性分析
4.7 实验对比与分析
4.8 小结
第5章 基于启发式On-the-fly的扩展TGBA模型检测算法
5.1 扩展的TGBA模型
5.2 MCA_ETGBA算法描述
5.3 算法实例
5.4 正确性证明及复杂度分析
5.5 实验
5.6 小结
第6章 基于场景分析的系统形式化模型生成方法
6.1 OCL与FSP简介
6.2 系统需求场景分析及形式化模型生成流程
6.3 系统需求场景的OCL分析子算法
6.4 系统形式化模型生成子算法
6.5 小结
第7章 基于LTS模型检测的系统安全性验证方法
7.1 系统安全性验证相关原理
7.2 基于模型检测的系统安全性验证方法
7.2.1 安全需求规格的形式化描述
7.2.2 基于LTS模型检测的安全性验证方法
7.3 实例研究
7.4 本章小结
第8章 基于故障注入的系统安全性分析
8.1 引言
8.2 基于故障注入的模型检测流程
8.3 基于故障注入的模型检测算法描述
8.4 多故障注入的算法实例
8.5 形式化安全需求规格的获取
8.6 本章小结
第9章 铁路车站联锁系统的安全性分析研究
9.1 安全性分析流程
9.2 铁路车站联锁系统中进路建立的形式化建模
9.2.1 铁路车站联锁系统进路建立场景
9.2.2 铁路车站联锁系统的进路建立需求场景分析
9.2.3 铁路车站联锁系统进路建立的形式化模型生成
9.3 铁路车站联锁系统中进路建立的安全性验证
9.4 系统的形式化安全需求
9.5 小结
第10章 结束语
参考文献