模型检测

模型检测是一种用于自动验证有限状态并发系统的技术，与基于模拟、测试和演绎推理的传统技术相比，具有许多方面的优势。本书涵盖的内容包括模型检测的基本知识、模态逻辑、符号化技术、SATSolver、限界模型检测、自动机上的模型检测、抽象解释、程序分析、实时系统验证，同时介绍NuSMV和UPPAAL两个流行的模型检测器。

Edmund M.Clarke教授，现任美国卡内基·梅隆大学计算机科学系教授，并且是ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉，2007年获得ACM图灵奖。
李刚，华北电力大学（保定）计算机系讲师，目前从事软件工程、建模与仿真、智能电网的信息化管理等方面的研究工作，主要内容是将计算机科学与技术的理论方法应用到电力系统的问题中，在智电网的故障诊断与预测方面，获得实用新型专利授权2项、计算机软件著作权1项。

第1章绪论
1.1形式化方法的需求
1.2硬件与软件验证
1.3模型检测的过程
1.4时序逻辑与模型检测
1.5符号算法
1.6偏序约简
1.7缓解状态爆炸问题的其他方法
第2章系统建模
2.1并发系统建模
2.2并发系统
2.3一个并发程序的Kripke模型
第3章时序逻辑
3.1计算树逻辑CLT*
3.2CTL和LTL
3.3公正性
第4章模型检测
4.1CTL模型检测
4.2用tableau进行LTL模型检测
4.3CTL*模型检测
第5章二叉判定图
5.1布尔公式的表示方法
5.2Kripke结构的表示方法
第6章符号模型检测
6.1不动点表示
6.2CTL符号模型检测
6.3符号模型检测中的公正性
6.4反例和诊断信息
6.5一个ALU的例子
6.6关系积的计算
6.7符号化的LTL模型检测
第7章基于μ-演算的模型检测
7.1简介
7.2命题μ-演算
7.3求不动点公式的值
7.4用OBDD表示μ-演算公式
7.5将CTL公式转化为μ-演算
7.6复杂度问题
第8章实际中的模型检测
8.1模型检测器——SMV
8.2一个实际的例子
第9章模型检测和自动机理论
9.1有限字与无限字上的自动机
9.2用自动机进行模型检测
9.3检查Büchi自动机接受的语言是否为空
9.4LTL公式转化为自动机
9.5“on-the-fly”模型检测
9.6检测语言包含的符号方法
第10章偏序约简
10.1异步系统中的并发
10.2独立性与不可见性
10.3LTL-X的偏序约简
10.4一个例子
10.5计算Ample集合
10.6算法的正确性
10.7SPIN系统中的偏序约简
第11章结构间的等价性和拟序
11.1等价和拟序算法
11.2构建tableau结构
第12章组合推理
12.1结构的组合
12.2假设保证方法的证明
12.3CPU控制器的验证
第13章抽象
13.1影响锥化简
13.2数值抽象
第14章对称性
14.1群和对称性
14.2商模型
14.3对称性和模型检测
14.4复杂性问题
14.5试验结果
第15章有限状态系统的无限簇
15.1无限簇上的时序逻辑
15.2不变量
15.3再次分析Futurebus+
15.4图和网络文法
15.5令牌环簇的不确定性结果
第16章离散实时系统和定量时序分析
16.1实时系统和单调变化率调度
16.2实时系统的模型检测
16.3RTCTL模型检测
16.4量化时序的分析：最小或最大延迟
16.5飞行控制器
第17章连续实时系统
17.1时间约束自动机
17.2并行组合
17.3使用时间约束自动机进行建模
17.4时钟域
17.5时钟区
17.6边界可区分矩阵
17.7对复杂度的考虑
第18章结论
参考文献