形式化方法导论PDF电子书下载

第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