工业关键系统的形式化方法--应用综述/国际信息工程先进技术译丛

形式化方法以数学为基础，其目标是建立精确的 、无二义性的语义，对系统开发的各个阶段进行有效 地描述，使系统的结构具有先天的合理性、正确性和 良好的维护性，能较好地满足用户需求。《工业关键 系统的形式化方法－－应用综述》记录和展示了作者 格涅斯和玛格丽特关于形式化方法如何在工业关键系 统中进行应用的研究成果。 本书分为6部分。第1部分是概述；第2部分致力 于介绍建模范例；第3部分介绍了包括形式化方法和 相关工具的使用以及应用程序在实际系统领域的发展 ；第4部分则向读者展示了形式化方法在通信系统中 的发展和成果；第5部分则介绍了形式化方法在互联 网和在线服务方面的应用；而在第6部分则介绍了实 时应用程序的形式化方法。 本书可用作高等院校计算机科学、自动化相关专 业本科生、研究生以及教师的参考用书，也可作为业 内专业人士的参考书。

Tiziana Margaria是波茨坦大学数学和自然科学学院的教授，主要负责信息学院的服务和软件工程学科，曾在德国哥廷根大学、多特蒙德工业大学和帕绍大学以及瑞典和意大利的大学访学。 Stefania Gnesi曾在佛罗伦萨大学任教，主要讲授针对软件系统分析和规范的方法和工具，现为意大利比萨ISTICNR形式化方法和工具实验室的负责人之一。

译者序 原书序 原书前言 第一部分 前言和发展现状 第一章 形式化方法：应用{逻辑关系，理论}的计算机科学 1.1 前言和发展现状 1.2 未来发展方向 致谢 参考文献 第二部分 建模范式 第二章 一种正在应用的同步语言：LUSTRE的发展 2.1 前言 2.2 同步语言风格 2.3 LUSTR和SCADE的设计和开发 2.3.1 工业发展 2.3.2 研究阶段 2.4 工业应用案例 2.4.1 预期成果 2.4.2 意外功能和需求 2.5 现状 第三章 群智能方法形式化集成要求 3.1 前言 3.2 群体技术 3.2.1 ANTS任务概述 3.2.2 ANTS规范和验证 3.3 美国宇航局（NASA）FAST项目 3.4 群体形式化集成方法 3.4.1 CSP简述 3.4.2 WSCCS简述 3.4.3 X-机 3.4.4 unity逻辑 3.5 结论 致谢 参考文献 第三部分 交通运输系统 第四章 形式化方法在铁路交通信号中的应用趋势 4.1 前言 4.2 CENELEC准则 4.3 铁路信号系统软件采购 4.3.1 系统分类 4.3.2 需求分析和规范 4.4 成功案例：B方法 4.5 铁路信号设备分类 4.5.1 列车控制系统 4.5.2 联锁系统 4.5.3 EURIS语言 4.6 结论 参考文献 第五章 航空电子设备的符号模型校验 5.1 前言 5.2 飞行跑道安全监控应用 5.2.1 RSM的作用 5.2.2 RSM的设计 5.2.3 RSM的形式化验证 5.2.4 符号模型校验结构 5.2.5 符号状态空间生成饱和算法 5.2.6 基于饱和算法的模型校验 5.2.7 随机模型校验可靠性和定时分析工具(SmArT) 5.3 RSM的离散模型 5.3.1 整型变量和实型变量抽象化 5.3.2 RSM的SMART模型 5.3.3 RSM模型校验 5.4 探讨80 5.4.1 经验教训 5.4.2 投入程度 5.4.3 故障容错 5.4.4 面临挑战 参考文献 第四部分 电信系统 第六章 形式化方法在有源网络电信服务中的应用 6.1 概述 6.2 有源网络 6.3 Capsule法 6.4 有源网络的之前分析方法 6.4.1 Maude 6.4.2 ACTIVESPEC 6.4.3 Unity 6.4.4 Verisim法 6.5 SPIN有源网络模型校验 6.5.1 PROMELA中的有源网络模型 6.5.2 实例：验证主动协议 6.5.3 在SPIN中更实际的代码建模 6.6 结论 参考文献 第七章 通信协议概率模型校验的实际应用 7.1 前言 7.2 PTAs 7.3 概率模型校验 7.3.1 概率模型校验技术 7.3.2 概率模型校验工具 7.4 案例分析:CSMA/CD 7.4.1 协议 7.4.2 PTA模型 7.4.3 模型分析 7.5 讨论和结论 致谢 参考文献 第五部分 互联网与在线服务 第八章 可验证性设计：在线会议系统案例分析 8.1 前言 8.2 用户模型 8.3 模型与框架 8.4 模型校验 8.5 通过自动机学习的应急全局行为验证 8.5.1 学习设置 8.5.2 学习行为模型 8.5.3 便于领域知识的自动机学习 8.6 相关工作 8.6.1 基于特征的系统 8.6.2 在线会议系统 8.6.3 政策 8.7 结论和展望 参考文献 第九章 随机模型校验在工业中的应用:用户中心建模和THINKTEAM中的合作分析 9.1 前言 9.2 THINKTEAM 9.2.1 技术特点 9.2.2 thinkteam的工作过程 9.3 thinkteam日志文件分析 9.4 具有复制仓库的thinkteam 9.4.1 thinkteam的随机模型 9.4.2 随机模型分析 9.5 经验教训 9.6 总结 致谢 参考文献 第六部分 运行时：测试和模型学习 第十章 测试和测试控制符号TTCN-3及其应用 10.1 前言 10.2 TTCN-3概念 10.2.1 模块 10.2.2 测试系统 10.2.3 测试案例和测试判决 10.2.4 备选方案和快照 10.2.5 缺省处理 10.2.6 通信操作 10.2.7 测试数据规范 10.3 入门示例 10.4 TTCN-3语义及其应用 10.5 TTCN-3的分布式测试平台 10.6 案例分析I：开放式服务架构（OSA）/增值服务测试 10.7 案例分析II：IP多媒体子系统（IMS）装置测试 10.8 结论 参考文献 第十一章 主动自动机学习的实际应用 11.1 前言 11.2 常规外推法 11.2.1 充分行为建模 11.3 常规外推法的挑战 11.3.1 等价查询注释 11.4 与实际系统交互 11.4.1 测试驱动程序设计示例 11.5 隶属度查询 11.5.1 冗余度 11.5.2 前缀闭包 11.5.3 行为独立性 11.5.4 确定性输入 11.5.5 对称性 11.5.6 滤波器示例 11.6 重置 11.6.1 重置示例 11.7 参数和值域 11.7.1 参数化示例 11.8 NGLL 11.8.1 基本技术 11.8.2 建模学习设置 11.9 总结和展望 参考文献