第1章 引言 1
1.1形式化方法 2
1.2开发与学习形式化方法 3
1.3使用形式化方法 5
1.4应用形式化方法 6
1.5本书概要 7
第2章 预备知识 8
2.1集合表示法 8
2.2字符串和语言 9
2.3图 10
2.4计算复杂度和可计算性 12
2.5扩展阅读 16
第3章 逻辑和定理证明 17
3.1一阶逻辑 17
3.2项 17
3.2.1赋值和解释 18
3.2.2多个论域上的结构 19
3.3一阶公式 19
3.4命题逻辑 23
3.5证明一阶逻辑公式 24
3.5.1正向推理 25
3.5.2反向推理 26
3.6证明系统的属性 26
3.6.1正确性 27
3.6.2完备性 27
3.6.3可判定性 27
3.6.4结构完备性 28
3.7证明命题逻辑属性 28
3.8一个实用的证明系统 29
3.9证明示例 31
3.10机器辅助证明 37
3.11机械化定理证明器 39
3.12扩展阅读 39
第4章 软件系统建模 40
4.1顺序系统、并发系统及反应式系统 41
4.2状态 42
4.3状态空间 43
4.4转换系统 44
4.5转换的粒度 47
4.6为程序建模的例子 48
4.6.1整数除法 48
4.6.2计算组合数 49
4.6.3 Eratosthenes筛法 50
4.6.4互斥 52
4.7非确定性转换 53
4.8将命题变量赋给状态 54
4.9合并状态空间 55
4.10线性视角 56
4.11分支视角 57
4.12公平性 58
4.13偏序视角 61
4.13.1一个银行系统的例子 61
4.13.2线性化和全局状态 63
4.13.3一个简单的例子 64
4.13.4偏序模型的应用 65
4.14形式化建模 65
4.15一个项目的建模 67
4.16扩展阅读 68
第5章 形式化规约 69
5.1规约机制的属性 69
5.2线性时序逻辑 70
5.3公理化LTL 74
5.4 LTL规约示例 74
5.4.1交通灯 74
5.4.2顺序程序的属性 75
5.4.3互斥 76
5.4.4公平性条件 76
5.5无限字上的自动机 77
5.6使用Buchi自动机作为规约 79
5.7确定性Buchi自动机 80
5.8其他规约机制 81
5.9复杂的规约 83
5.10规约的完整性 83
5.11扩展阅读 84
第6章 自动验证 85
6.1状态空间搜索 86
6.2状态表示方法 87
6.3自动机结构体系 88
6.4合并Buchi自动机 89
6.4.1广义Buchi自动机 90
6.4.2将广义Buchi自动机转换为简单Buchi自动机 91
6.5 Buchi自动机求补 92
6.6检验空集 93
6.7模型检验范例 94
6.8将LTL转换为自动机 95
6.9模型检验的复杂度 100
6.10表示公平性 102
6.11检验LTL规约 102
6.12安全属性 103
6.13状态空间爆炸问题 104
6.14模型检验的优点 105
6.15模型检验的缺点 105
6.16选择自动验证工具 105
6.17模型检验项目 105
6.18模型检验工具 106
6.19扩展阅读 106
第7章 演绎式软件验证 107
7.1流程图程序的验证 107
7.2含数组变量的验证 111
7.2.1含数组变量赋值的问题 112
7.2.2修改证明系统 112
7.3完全正确性 114
7.4公理式程序验证 117
7.4.1赋值公理 117
7.4.2空语句公理 117
7.4.3左强化规则 117
7.4.4右弱化规则 118
7.4.5顺序组合规则 118
7.4.6 if-then-else规则 118
7.4.7 while规则 118
7.4.8 begin-end规则 119
7.4.9示例：整数除法 119
7.5并发程序的验证 121
7.6演绎验证的优点 124
7.7演绎验证的缺点 125
7.8证明系统的正确性和完备性 126
7.9组合性 127
7.10演绎验证工具 128
7.11扩展阅读 128
第8章 进程代数与等价关系 129
8.1进程代数 130
8.2通信系统的演算 131
8.2.1动作前缀 131
8.2.2选择 132
8.2.3并发组合 132
8.2.4限制符 133
8.2.5重标记 133
8.2.6等式定义 133
8.2.7 agent 0 135
8.2.8传值agent 135
8.3示例：Dekker算法 135
8.4建模问题 137
8.5 agent之间的等价性 138
8.5.1迹等价 139
8.5.2失败等价 139
8.5.3模拟等价 140
8.5.4互模拟和弱互模拟等价 142
8.6等价关系的层级 142
8.7用进程代数研究并发 143
8.8计算互模拟等价 145
8.9 LOTOS 147
8.10进程代数工具 148
8.11扩展阅读 148
第9章 软件测试 150
9.1审查和走查 151
9.2控制流覆盖准则 152
9.2.1语句覆盖 153
9.2.2边覆盖 153
9.2.3条件覆盖 153
9.2.4边/条件覆盖 154
9.2.5条件组合覆盖 154
9.2.6路径覆盖 154
9.2.7不同覆盖准则的比较 155
9.2.8循环覆盖 155
9.3数据流覆盖准则 155
9.4传播路径条件 157
9.4.1示例：GCD程序 159
9.4.2含有输入语句的路径 160
9.5等价类划分 160
9.6待测代码预处理 160
9.7检查测试套件 161
9.8组合性 162
9.9黑盒测试 163
9.10概率测试 164
9.11测试的优点 165
9.12测试的缺点 166
9.13测试工具 166
9.14扩展阅读 166
第10章 组合形式化方法 167
10.1抽象 167
10.2组合测试与模型检验 171
10.2.1直接检验 171
10.2.2黑盒系统 172
10.2.3组合锁自动机 172
10.2.4黑盒死锁检测 172
10.2.5一致性测试 173
10.2.6检验重置的可靠性 175
10.2.7黑盒检验 176
10.3净室方法 177
10.3.1验证 177
10.3.2证明审查 177
10.3.3测试 177
10.4扩展阅读 178
第11章 可视化 179
11.1在形式化方法中运用可视化 179
11.2消息序列图 180
11.3可视化流程图和状态机 182
11.4层次状态图 184
11.4.1层次化状态 184
11.4.2统一的出口和入口 185
11.4.3并发 185
11.4.4输入和输出 185
11.5程序文本的可视化 186
11.6 Petri网 186
11.7可视化工具 188
11.8扩展阅读 188
结束语 189
参考文献 191