模型检测(model checking)，是一种很重要的自动验证技术。它最早由Clarke和Emerson以及Quelle和Sifakis在1981年分别提出，主要通过显式状态搜索或隐式不动点计算来验证有穷状态并发系统的模态/命题性质。由于模型检测可以自动执行，并能在系统不满足性质时提供反例路径，因此在工业界比演绎证明更受推崇。
尽管限制在有穷系统上是一个缺点，但模型检测可以应用于许多非常重要的系统，如硬件控制器和通信协议等有穷状态系统。很多情况下，可以把模型检测和各种抽象与归纳原则结合起来验证非有穷状态系统(如实时系统)。

作译者：吴尽昭 等
出版时间：2018-11千 字 数：346版次：01-01页 数：240
开本：16开装帧：I S B N ：9787121352744
换版：
纸质书定价：￥69.0
模型检测是一种用于自动验证有限状态并发系统的技术，与基于模拟、测试和演绎推理的传统技术相比，具有许多方面的优势。本书共分18章，涵盖的主要内容包括模型检测的基本知识、模态逻辑、符号化技术、SATSolver、限界模型检测、自动机上的模型检测、抽象解释、程序分析、实时系统验证，同时介绍NuSMV和UPPAAL两个流行的模型检测器。
第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.2 CTL和LTL逻辑 20
3.3 公正性 22
第4章 模型检测 24
4.1 CTL模型检测 24
4.2 基于tableau结构的LTL模型检测 29
4.3 CTL*模型检测 33
第5章 二叉判定图 36
5.1 布尔公式的表示方法 36
5.2 Kripke结构的表示方法 40
第6章 符号模型检测 42
6.1 不动点表示 42
6.2 CTL符号模型检测 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.1 SMV模型检测器 77
8.2 一个实际的例子 80
第9章 模型检测和自动机理论 85
9.1 有限字与无限字上的自动机 85
9.2 使用自动机进行模型检测 86
9.3 检查Büchi自动机接受的语言是否为空 90
9.4 LTL公式转化为自动机 93
9.5 采用“On-the-Fly”技术的模型检测 97
9.6 检测语言包含的符号方法 98
第10章 偏序约简 100
10.1 异步系统中的并发 101
10.2 独立性与不可见性 102
10.3 LTL?X的偏序约简 104
10.4 一个例子 107
10.5 计算充足集(ample)集合 109
10.6 算法的正确性 114
10.7 SPIN系统中的偏序约简 117
第11章 结构间的等价性和拟序 122
11.1 等价和拟序算法 128
11.2 构建tableau结构 129
第12章 组合推理 133
12.1 多个结构的组合 134
12.2 判断假设保证证明方法的正确性 136
12.3 CPU控制器的验证 136