工业关键系统的形式化方法：应用综述

形式化方法以数学为基础，其目标是建立精确的、无二义性的语义，对系统开发的各个阶段进行有效地描述，使系统的结构具有先天的合理性、正确性和良好的维护性，能较好地满足用户需求。本书记录和展示了作者关于形式化方法如何在工业关键系统中进行应用的研究成果。
　　
　　本书分为6部分。第1部分是概述；第2部分致力于介绍建模范例；第3部分介绍了包括形式化方法和相关工具的使用以及应用程序在实际系统领域的发展；第4部分则向读者展示了形式化方法在通信系统中的发展和成果；第5部分则介绍了形式化方法在互联网和在线服务方面的应用；而在第6部分则介绍了实时应用程序的形式化方法。
　　
　　本书可用作高等院校计算机科学、自动化相关专业本科生、研究生以及教师的参考用书，也可作为业内专业人士的参考书。
　　
　　译者序
　　
　　原书序
　　
　　原书前言
　　
　　第一部分前言和发展现状
　　
　　第一章形式化方法：应用{逻辑关系，理论}的计算机科学
　　
　　1.1前言和发展现状
　　
　　1.2未来发展方向
　　
　　致谢
　　
　　参考文献
　　
　　第二部分建模范式
　　
　　第二章一种正在应用的同步语言：LUSTRE的发展
　　
　　2.1前言
　　
　　2.2同步语言风格
　　
　　2.3LUSTR和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.2ANTS规范和验证
　　
　　3.3美国宇航局（NASA）FAST项目
　　
　　3.4群体形式化集成方法
　　
　　3.4.1CSP简述
　　
　　3.4.2WSCCS简述
　　
　　3.4.3X-机
　　
　　3.4.4unity逻辑
　　
　　3.5结论
　　
　　致谢
　　
　　参考文献
　　
　　第三部分交通运输系统
　　
　　第四章形式化方法在铁路交通信号中的应用趋势
　　
　　4.1前言
　　
　　4.2CENELEC准则
　　
　　4.3铁路信号系统软件采购
　　
　　4.3.1系统分类
　　
　　4.3.2需求分析和规范
　　
　　4.4成功案例：B方法
　　
　　4.5铁路信号设备分类
　　
　　4.5.1列车控制系统
　　
　　4.5.2联锁系统
　　
　　4.5.3EURIS语言
　　
　　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.3RSM的离散模型
　　
　　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.3Capsule法
　　
　　6.4有源网络的之前分析方法
　　
　　6.4.1Maude
　　
　　6.4.2ACTIVESPEC
　　
　　6.4.3Unity
　　
　　6.4.4Verisim法
　　
　　6.5SPIN有源网络模型校验
　　
　　6.5.1PROMELA中的有源网络模型
　　
　　6.5.2实例：验证主动协议
　　
　　6.5.3在SPIN中更实际的代码建模
　　
　　6.6结论
　　
　　参考文献
　　
　　第七章通信协议概率模型校验的实际应用
　　
　　7.1前言
　　
　　7.2PTAs
　　
　　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.2THINKTEAM
　　
　　9.2.1技术特点
　　
　　9.2.2thinkteam的工作过程
　　
　　9.3thinkteam日志文件分析
　　
　　9.4具有复制仓库的thinkteam
　　
　　9.4.1thinkteam的随机模型
　　
　　9.4.2随机模型分析
　　
　　9.5经验教训
　　
　　9.6总结
　　
　　致谢
　　
　　参考文献
　　
　　第六部分运行时：测试和模型学习
　　
　　第十章测试和测试控制符号TTCN-3及其应用
　　
　　10.1前言
　　
　　10.2TTCN-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.4TTCN-3语义及其应用
　　
　　10.5TTCN-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.8NGLL
　　
　　11.8.1基本技术
　　
　　11.8.2建模学习设置
　　
　　11.9总结和展望
　　
　　参考文献

邮购信息：
　　地    址：北京市西城区北三环中路甲29号华尊大厦A座405室(邮编：100029)
　　电    话：010-82024981-12  发行部
       邮    箱：wangy@upsapp.com
　　户    名：北京三之联广告有限公司
　　开户行：交通银行股份有限公司北京北三环中路支行
　　账   号：110060567018150018791

ISBN：978-7-111-48521-6   出版社：机械工业出版社     出版日期：2015-1-12 装帧：平装    定价：￥69.00 类别：通信