第1章 绪论 1
1.1 形式化方法的发展历程 1
1.2 形式化方法的基本内容 3
1.2.1 系统建模 3
1.2.2 形式规约 4
1.2.3 形式验证 5
1.3 本章小结 7
习题1 8
第2章 程序正确性证明 9
2.1 前后断言法 10
2.1.1 基本概念 10
2.1.2 证明方法 10
2.1.3 应用举例 12
2.2 公理化方法 14
2.2.1 基本概念 14
2.2.2 证明方法 14
2.2.3 应用举例 16
2.3 最弱前置条件方法 19
2.3.1 基本概念 19
2.3.2 证明方法 22
2.3.3 应用举例 24
2.4 本章小结 25
习题2 25
上篇 系统建模 29
第3章 迁移系统 29
3.1 基本概念 29
3.1.1 形式定义 29
3.1.2 迁移图 31
3.1.3 计算 32
3.2 应用举例 33
3.2.1 时序电路 34
3.2.2 数据依赖系统 35
3.2.3 并发和交错 38
3.3 本章小结 42
习题3 43
第4章 自动机 44
4.1 有穷自动机 44
4.1.1 有穷状态系统 44
4.1.2 形式定义 46
4.1.3 判定算法 52
4.2 Büchi自动机 53
4.2.1 ω-有穷自动机简介 53
4.2.2 Büchi自动机 53
4.2.3 应用举例 57
4.3 本章小结 59
习题4 59
第5章 Petri网 60
5.1 库所／变迁Petri网 60
5.1.1 基本概念 60
5.1.2 基本性质 64
5.1.3 分析方法 65
5.1.4 应用举例 69
5.2 谓词／变迁Petri网 70
5.2.1 基本概念 70
5.2.2 应用举例 70
5.3 着色Petri网 72
5.3.1 基本概念 72
5.3.2 应用举例 73
5.4 本章小结 74
习题5 74
中篇 形式规约 77
第6章 时序逻辑 77
6.1 线性时序逻辑 78
6.1.1 LTL语法 78
6.1.2 LTL语义 79
6.1.3 应用举例 83
6.2 分支时序逻辑 85
6.2.1 CTL语法 85
6.2.2 CTL语义 86
6.2.3 应用举例 88
6.3 区间时序逻辑简介 89
6.4 本章小结 91
习题6 91
第7章 并发系统属性 93
7.1 基本概念 93
7.2 安全性 95
7.2.1 形式定义 95
7.2.2 形式描述 96
7.2.3 应用举例 98
7.3 活性 99
7.3.1 形式定义 99
7.3.2 形式描述 100
7.3.3 应用举例 101
7.4 本章小结 102
习题7 103
下篇 形式验证 107
第8章 演绎证明 107
8.1 演绎证明方法 107
8.1.1 PLTL逻辑系统 107
8.1.2 Manna-Pnueli演绎规则方法 110
8.1.3 验证图方法 112
8.1.4 应用举例 113
8.2 验证工具STeP 118
8.2.1 STeP简介 118
8.2.2 STeP使用 118
8.3 STeP应用举例 121
8.3.1 建模 122
8.3.2 验证 124
8.4 本章小结 126
习题8 127
第9章 模型检测 128
9.1 基本概念 128
9.2 模型检测算法 129
9.2.1 CTL模型检测算法 130
9.2.2 LTL模型检测算法 140
9.3 模型检测工具及应用 153
9.3.1 验证工具SPIN 153
9.3.2 应用举例 162
9.4 本章小结 166
习题9 167
第10章 符号模型检测 168
10.1 二叉决策图 169
10.1.1 基本概念 169
10.1.2 约简方法 171
10.1.3 Apply操作及应用 174
10.2 CTL符号模型检测 177
10.2.1 基本方法 177
10.2.2 验证工具SMV 182
10.2.3 应用举例 185
10.3 LTL符号模型检测简介 187
10.4 本章小结 191
习题10 192
第11章 概率模型检测 193
11.1 概率模型 193
11.1.1 离散时间马尔可夫链 193
11.1.2 马尔可夫决策过程 195
11.1.3 连续时间马尔可夫链 197
11.2 概率时序逻辑 201
11.2.1 概率计算树逻辑 201
11.2.2 连续随机逻辑 204
11.3 概率模型检测工具及应用 206
11.3.1 验证工具PRISM 206
11.3.2 应用举例 221
11.4 本章小结 225
习题11 225
第12章 实时与混成系统验证 227
12.1 时间自动机 227
12.1.1 语法 227
12.1.2 语义 228
12.2 实时逻辑 229
12.2.1 时间计算树逻辑 230
12.2.2 度量区间时序逻辑 232
12.3 实时系统模型检测 234
12.3.1 基本方法 234
12.3.2 验证工具UPPAAL 240
12.3.3 应用举例 244
12.4 混成系统验证简介 246
12.4.1 混成自动机 246
12.4.2 微分动态逻辑 249
12.4.3 混成系统模型检测 252
12.5 本章小结 253
习题12 254
参考文献 255