Büchi自动机模型检测及其安全性分析应用研究

第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章 结束语
参考文献