国际信息工程先进技术译丛 工业关键系统的形式化方法：应用综述
作者：（意）Stefania Gnesi，Tiziana Margaria 著
出版时间：2015
丛编项： 国际信息工程先进技术译丛
内容简介
　　形式化方法以数学为基础，其目标是建立精确的、无二义性的语义，对系统开发的各个阶段进行有效地描述，使系统的结构具有先天的合理性、正确性和良好的维护性，能较好地满足用户需求。《工业关键系统的形式化方法：应用综述》记录和展示了作者关于形式化方法如何在工业关键系统中进行应用的研究成果。
　　《工业关键系统的形式化方法：应用综述》分为6部分。第1部分是概述；第2部分致力于介绍建模范例；第3部分介绍了包括形式化方法和相关工具的使用以及应用程序在实际系统领域的发展；第4部分则向读者展示了形式化方法在通信系统中的发展和成果；第5部分则介绍了形式化方法在互联网和在线服务方面的应用；而在第6部分则介绍了实时应用程序的形式化方法。
　　《工业关键系统的形式化方法：应用综述》可用作高等院校计算机科学、自动化相关专业本科生、研究生以及教师的参考用书，也可作为业内专业人士的参考书。
目录
译者序
原书序
原书前言
第一部分 前言和发展现状
第一章 形式化方法：应用{逻辑关系，理论}的计算机科学
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.1ANTS任务概述
3.2.2 ANTS规范和验证
3.3 美国宇航局（NASA）FAST项目
3.4群体形式化集成方法
3.4.1 CSP简述
3.4.2WSCCS 简述
3.4.3X-机
3.4.4unity逻辑
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.1RSM的作用
5.2.2RSM的设计
5.2.3RSM的形式化验证
5.2.4符号模型校验结构
5.2.5符号状态空间生成饱和算法
5.2.6基于饱和算法的模型校验
5.2.7随机模型校验可靠性和定时分析工具(SmArT)
5.3 RSM的离散模型
5.3.1整型变量和实型变量抽象化
5.3.2RSM的SMART模型
5.3.3RSM模型校验
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.1Maude
6.4.2 ACTIVESPEC
6.4.3 Unity
6.4.4Verisim法
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.2PTA模型
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.2thinkteam 的工作过程
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 总结和展望
参考文献