模型检测【2025|PDF下载-Epub版本|mobi电子书|kindle百度云盘下载】

模型检测PDF格式电子书版下载

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

第1章 绪论1

1.1 形式化方法的需求1

1.2 硬件与软件验证1

1.3 模型检测的过程3

1.4 时序逻辑与模型检测3

1.5 符号算法5

1.6 偏序约简6

1.7 缓解状态爆炸问题的其他方法7

第2章 系统建模9

2.1 并发系统建模9

2.2 并发系统12

2.3 一个并发程序的Kripke模型17

第3章 时序逻辑19

3.1 计算树逻辑CLT＊19

3.2 CTL和LTL21

3.3 公正性23

第4章 模型检测25

4.1 CTL模型检测25

4.2 用tableau进行LTL模型检测30

4.3 CTL＊模型检测34

第5章 二叉判定图37

5.1 布尔公式的表示方法37

5.2 Kripke结构的表示方法41

第6章 符号模型检测43

6.1 不动点表示43

6.2 CTL符号模型检测47

6.3 符号模型检测中的公正性49

6.4 反例和诊断信息51

6.5 一个ALU的例子53

6.6 关系积的计算55

6.7 符号化的LTL模型检测62

第7章 基于μ－演算的模型检测69

7.1 简介69

7.2 命题μ－演算70

7.3 求不动点公式的值72

7.4 用OBDD表示μ－演算公式75

7.5 将CTL公式转化为μ－演算76

7.6 复杂度问题77

第8章 实际中的模型检测78

8.1 模型检测器——SMV78

8.2 一个实际的例子81

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

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

9.2 用自动机进行模型检测87

9.3 检查Büchi自动机接受的语言是否为空91

9.4 LTL公式转化为自动机94

9.5 采用“on-the-fly”技术的模型检测98

9.6 检测语言包含的符号方法99

第10章 偏序约简101

10.1 异步系统中的并发102

10.2 独立性与不可见性103

10.3 LTL-x的偏序约简105

10.4 一个例子108

10.5 计算Ample集合110

10.6 算法的正确性115

10.7 SPIN系统中的偏序约简118

第11章 结构间的等价性和拟序123

11.1 等价和拟序算法129

11.2 构建tableau结构130

第12章 组合推理134

12.1 结构的组合135

12.2 假设保证方法的证明136

12.3 CPU控制器的验证137

第13章 抽象139

13.1 影响锥化简139

13.2 数值抽象141

第14章 对称性153

14.1 群和对称性153

14.2 商模型156

14.3 对称性和模型检测158

14.4 复杂性问题159

14.5 试验结果163

第15章 有限状态系统的无限簇165

15.1 无限簇上的时序逻辑165

15.2 不变量166

15.3 再次分析Futurebus＋168

15.4 图和网络文法170

15.5 令牌环簇的不确定性结果178

第16章 离散实时系统和定量时序分析182

16.1 实时系统和单调变化率调度182

16.2 实时系统的模型检测183

16.3 RTCTL模型检测184

16.4 量化时序的分析：最小或最大延迟184

16.5 飞行控制器186

第17章 连续实时系统191

17.1 时间约束自动机191

17.2 并行组合193

17.3 使用时间约束自动机进行建模194

17.4 时钟域197

17.5 时钟区202

17.6 边界可区分矩阵207

17.7 对复杂度的考虑210

第18章 结论211

参考文献213