模型检测PDF电子书下载

第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 S MV模型检测器 77

8.2 一个实际的例子 80

第9章 模型检测和自动机理论 85

9.1 有限字与无限字上的自动机 85

9.2 使用自动机进行模型检测 86

9.3 检查Buchi自动机接受的语言是否为空 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

第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.3 RTCTL模型检测 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