模型检测

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

埃德蒙·M.克拉克教授，美国卡内基·梅隆大学计算机科学系教授，并且是ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉，2007年获得ACM图灵奖。

第1章绪论1
1.1形式化方法的需求1
1.2硬件与软件验证1
1.3模型检测的流程3
1.4时序逻辑与模型检测3
1.5符号算法4
1.6偏序约简6
1.7缓解状态爆炸问题的其他方法7
第2章系统建模8
2.1并发系统建模8
2.2并发系统11
2.3程序翻译的实例16
第3章时序逻辑18
3.1计算树逻辑CTL*18
3.2CTL和LTL逻辑20
3.3公正性22
第4章模型检测24
4.1CTL模型检测24
4.2基于tableau结构的LTL模型检测29
4.3CTL*模型检测33
第5章二叉判定图36
5.1布尔公式的表示方法36
5.2Kripke结构的表示方法40
第6章符号模型检测42
6.1不动点表示42
6.2CTL符号模型检测45
6.3符号模型检测中的公正性48
6.4反例和诊断信息50
6.5一个ALU的例子52
6.6关系积的计算54
6.7符号化的LTL模型检测61
第7章基于μ演算的模型检测68
7.1简介68
7.2命题μ演算68
7.3求不动点公式的值71
7.4用OBDD表示μ演算公式74
7.5将CTL公式转化为μ演算75
7.6复杂度问题76
第8章实践中的模型检测77
8.1SMV模型检测器77
8.2一个实际的例子80
第9章模型检测和自动机理论85
9.1有限字与无限字上的自动机85
9.2使用自动机进行模型检测86
9.3检查Büchi自动机接受的语言是否为空90
9.4LTL公式转化为自动机93
9.5采用“On-the-Fly”技术的模型检测97
9.6检测语言包含的符号方法98
第10章偏序约简100
10.1异步系统中的并发101
10.2独立性与不可见性102
10.3LTL?X的偏序约简104
10.4一个例子107
10.5计算充足集(ample)集合109
10.6算法的正确性114
10.7SPIN系统中的偏序约简117
第11章结构间的等价性和拟序122
11.1等价和拟序算法128
11.2构建tableau结构129
第12章组合推理133
12.1多个结构的组合134
12.2判断假设保证证明方法的正确性136
12.3CPU控制器的验证136
第13章抽象139
13.1影响锥化简139
13.2数值抽象141
第14章对称性154
14.1群和对称性154
14.2商模型156
14.3对称性和模型检测159
14.4复杂度问题160
14.5实验结果164
第15章有限状态系统的无限簇166
15.1无限簇上的时序逻辑166
15.2不变量167
15.3再次分析Futurebus+169
15.4图和网络文法171
15.5令牌环簇的不确定性结果179
第16章离散实时系统和定量时序分析183
16.1实时系统和单调变化率调度183
16.2实时系统的模型检测184
16.3RTCTL模型检测185
16.4量化时序的分析：最小或优选延迟185
16.5飞行控制器187
第17章连续实时系统192
17.1时间约束自动机192
17.2并行组合194
17.3使用时间约束自动机进行建模195
17.4时钟域198
17.5时钟区203
17.6边界可区分矩阵208
17.7复杂度问题211
第18章结论213
参考文献215