Büchi自动机模型检测及其安全性分析应用研究PDF电子书下载

查看更多关于的内容

第1章 绪论 1

1.1 研究背景 1

1.2 国内外研究现状 2

1.2.1 模型检测相关研究 2

1.2.2 安全苛求系统的安全性研究现状 7

1.2.3 模型检测与安全性分析研究现状 12

1.3 研究内容 14

1.4 本书的结构安排 17

第2章 基于Büchi自动机的模型检测理论与方法 21

2.1 Büchi自动机基本原理 21

2.1.1 标准Büchi自动机 21

2.1.2 广义Büchi自动机 22

2.2 模型检测基本原理 23

2.2.1 系统建模 23

2.2.2 属性描述 24

2.2.3 模型验证 27

2.3 基于LTL的模型检测 28

2.4 基于Büchi自动机的模型检测方法 29

2.5 本章小结 30

第3章 基于启发式NDFS的模型检测算法 31

3.1 NDFS模型检测算法研究现状 31

3.2 基本概念及相关技术 33

3.2.1 TGBA简介 33

3.2.2 相关技术 33

3.3 HNDFS算法描述 37

3.4 HNDFS算法正确性证明 42

3.5 HNDFS算法复杂度分析 45

3.6 实验与分析 47

3.7 本章小结 49

第4章 基于启发式SCCs的广义Büchi自动机判空检测算法 50

4.1 引言 50

4.2 HSCCsEC算法描述 51

4.4 HSCCsEC算法实例 56

4.5 HSCCsEC算法正确性证明 59

4.6 HSCCsEC算法复杂性分析 62

4.7 实验对比与分析 64

4.8 小结 67

第5章 基于启发式on-the-fly的扩展TGBA模型检测算法 68

5.1 扩展的TGBA模型 69

5.2 MCA_ETGBA算法描述 69

5.3 算法实例 74

5.4 正确性证明及复杂度分析 78

5.5 实验 82

5.6 小结 84

第6章 基于场景分析的系统形式化模型生成方法 86

6.1 OCL与FSP简介 86

6.2 系统需求场景分析及形式化模型生成流程 88

6.3 系统需求场景的OCL分析子算法 88

6.4 系统形式化模型生成子算法 90

6.5 小结 92

第7章 基于LTS模型检测的系统安全性验证方法 93

7.1 系统安全性验证相关原理 93

7.2 基于模型检测的系统安全性验证方法 94

7.2.1 安全需求规格的形式化描述 94

7.2.2 基于LTS模型检测的安全性验证方法 95

7.3 实例研究 96

7.4 本章小结 99

第8章 基于故障注入的系统安全性分析 100

8.1 引言 100

8.2 基于故障注入的模型检测流程 100

8.3 基于故障注入的模型检测算法描述 102

8.4 多故障注入的算法实例 107

8.5 形式化安全需求规格的获取 108

8.6 本章小结 110

第9章 铁路车站联锁系统的安全性分析研究 111

9.1 安全性分析流程 111

9.2 铁路车站联锁系统中进路建立的形式化建模 113

9.2.1 铁路车站联锁系统进路建立场景 113

9.2.2 铁路车站联锁系统的进路建立需求场景分析 115

9.2.3 铁路车站联锁系统进路建立的形式化模型生成 120

9.3 铁路车站联锁系统中进路建立的安全性验证 125

9.4 系统的形式化安全需求 130

9.5 小结 130

第10章 结束语 131

参考文献 134

查看更多关于的内容