工业关键系统的形式化方法 应用综述PDF电子书下载

第1部分 概述和发展现状 3

第1章 形式化方法：应用｛逻辑关系，理论｝的计算机科学 3

1.1 概述 3

1.2 未来发展方向 7

致谢 9

参考文献 9

第2部分 建模范例 15

第2章 一种正在应用的同步语言：LUSTRE的发展 15

2.1 简介 15

2.2 同步语言风格 16

2.3 LUSTRE和SCADE的设计和开发 17

2.3.1 工业发展 18

2.3.2 研究阶段 19

2.4 工业应用案例 22

2.4.1 预期成果 22

2.4.2 意外功能和需求 23

2.5 现状 24

参考文献 25

第3章 群智能方法形式化集成要求 28

3.1 简介 28

3.2 群体技术 29

3.2.1 ANTS任务概述 30

3.2.2 ANTS规范和验证 31

3.3 NASA FAST项目 33

3.4 群体形式化集成方法 34

3.4.1 CSP简述 34

3.4.2 WSCCS简述 39

3.4.3 X机 42

3.4.4 Unity逻辑 45

3.5 小结 47

致谢 48

参考文献 48

第3部分 交通运输系统 55

第4章 形式化方法在铁路交通信号中的应用趋势 55

4.1 简介 55

4.2 CENELEC标准 56

4.3 铁路信号系统软件采购 57

4.3.1 系统分类 58

4.3.2 需求分析和规范 58

4.4 成功案例：B方法 60

4.5 铁路信号设备分类 61

4.5.1 列车控制系统 61

4.5.2 联锁系统 63

4.5.3 EURIS语言 66

4.6 小结 68

参考文献 69

第5章 航空电子设备的符号模型校验 73

5.1 简介 73

5.2 飞行跑道安全监控应用 74

5.2.1 RSM的作用 75

5.2.2 RSM的设计 75

5.2.3 RSM的形式化验证 76

5.2.4 符号模型校验结构 77

5.2.5 符号状态空间生成饱和算法 79

5.2.6 基于饱和算法的模型校验 81

5.2.7 随机模型校验可靠性和定时分析工具（SMART） 82

5.3 RSM的离散模型 82

5.3.1 整型变量和实型变量抽象化 82

5.3.2 RSM的SMART模型 83

5.3.3 RSM模型校验 89

5.4 探讨 93

5.4.1 经验教训 93

5.4.2 投入程度 93

5.4.3 故障容错 94

5.4.4 面临挑战 94

参考文献 94

第4部分 通信系统 101

第6章 形式化方法在有源网络通信服务中的应用 101

6.1 简介 101

6.2 有源网络 101

6.3 CAPSULE法 102

6.4 有源网络的之前分析方法 104

6.4.1 Maude 104

6.4.2 ActiveSPEC 105

6.4.3 Unity 105

6.4.4 Verisim法 106

6.5 SPIN有源网络模型校验 106

6.5.1 PROMELA中的有源网络模型 107

6.5.2 实例：验证主动协议 111

6.5.3 在SPIN中更实际的代码建模 112

6.6 小结 113

参考文献 114

第7章 通信协议概率模型校验的实际应用 116

7.1 简介 116

7.2 PTA 117

7.3 概率模型校验 118

7.3.1 概率模型校验技术 119

7.3.2 概率模型校验工具 120

7.4 案例分析：CSMA/CD 121

7.4.1 协议 121

7.4.2 PTA模型 122

7.4.3 模型分析 123

7.5 讨论和小结 127

致谢 128

参考文献 128

第5部分 互联网与在线服务 133

第8章 可验证性设计：在线会议系统案例分析 133

8.1 简介 133

8.2 用户模型 134

8.3 模型与框架 137

8.4 模型校验 138

8.5 通过自动机学习的应急全局行为验证 139

8.5.1 学习设置 140

8.5.2 学习行为模型 141

8.5.3 便于领域知识的自动机学习 144

8.6 相关工作 147

8.6.1 基于特征的系统 148

8.6.2 在线会议系统 148

8.6.3 政策 149

8.7 小结和展望 149

参考文献 150

第9章 随机模型校验在工业中的应用：用户中心建模和thinkteam中的合作分析 154

9.1 简介 154

9.2 thinkteam 156

9.2.1 技术特点 156

9.2.2 thinkteam的工作过程 157

9.3 thinkteam日志文件分析 158

9.4 具有复制仓库的thinkteam 163

9.4.1 thinkteam的随机模型 164

9.4.2 随机模型分析 167

9.5 经验教训 173

9.6 小结 173

致谢 174

参考文献 174

第6部分 运行时：测试和模型学习 179

第10章 测试和测试控制符号TTCN-3及其应用 179

10.1 简介 179

10.2 TTCN-3概念 182

10.2.1 模块 182

10.2.2 测试系统 183

10.2.3 测试案例和测试判决 184

10.2.4 备选方案和快照 184

10.2.5 默认处理 185

10.2.6 通信操作 185

10.2.7 测试数据规范 186

10.3 入门示例 187

10.4 TTCN-3语义及其应用 189

10.5 TTCN-3的分布式测试平台 190

10.6 案例分析Ⅰ：OSA／增值服务测试 192

10.7 案例分析Ⅱ：IMS装置测试 194

10.8 小结 198

参考文献 199

第11章 主动自动机学习的实际应用 202

11.1 简介 202

11.2 常规外推法 204

11.2.1 充分行为建模 207

11.3 常规外推法的挑战 208

11.3.1 等价查询注释 210

11.4 与实际系统交互 210

11.4.1 测试驱动程序设计示例 211

11.5 隶属度查询 213

11.5.1 冗余度 213

11.5.2 前缀闭包 213

11.5.3 行为独立性 214

11.5.4 确定性输入 215

11.5.5 对称性 215

11.5.6 滤波器示例 215

11.6 重置 216

11.6.1 重置示例 217

11.7 参数和值域 218

11.7.1 参数化示例 220

11.8 NGLL 221

11.8.1 基本技术 222

11.8.2 建模学习设置 222

11.9 小结和展望 224

参考文献 224