第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