工业关键系统的形式化方法

译者序原书序原书前言第一部分 前言和发展现状第一章 形式化方法：应用{逻辑关系，理论}的计算机科学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 探讨805.4.1 经验教训5.4.2 投入程度5.4.3 故障容错5.4.4 面临挑战参考文献第四部分 电信系统第六章形式化方法在有源网络电信服务中的应用6.1概述6.2 有源网络6.3 Capsule法6.4 有源网络的之前分析方法6.4.1Maude6.4.2 ACTIVESPEC6.4.3 Unity6.4.4Verisim法6.5 SPIN有源网络模型校验6.5.1 PROMELA中的有源网络模型6.5.2实例：验证主动协议6.5.3在SPIN中更实际的代码建模6.6结论参考文献第七章通信协议概率模型校验的实际应用7.1前言7.2 PTAs7.3概率模型校验7.3.1概率模型校验技术7.3.2概率模型校验工具7.4案例分析：CSMA / CD7.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 THINKTEAM9.2.1 技术特点9.2.2thinkteam 的工作过程9.3 thinkteam日志文件分析9.4 具有复制仓库的thinkteam9.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 NGLL11.8.1 基本技术11.8.2 建模学习设置11.9 总结和展望参考文献

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