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

基本信息

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

定价：69.00元

作者：格涅斯 (Stefania Gnesi)

出版社：机械工业出版社

出版日期：2015-01-01

ISBN：9787111485216

字数：

页码：226

版次：1

装帧：平装

开本：16

商品重量：0.4kg

编辑推荐

综合先进的文献资料和常用方法，案例均来自实际开发过程。

内容提要

形式化方法以数学为基础，其目标是建立的、无二义性的语义，对系统开发的各个阶段进行有效地描述，使系统的结构具有先天的合理性、正确性和良好的维护性，能较好地满足用户需求。本书记录和展示了作者关于形式化方法如何在工业关键系统中进行应用的研究成果。
本书分为6部分。部分是概述；第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 总结
致谢
参考文献
第六部分 运行时：测试和模型学习
第十章 测试和测试控制符号TT—3及其应用
10.1前言
10.2 TT—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 TT—3语义及其应用
10.5 TT—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 总结和展望
参考文献

作者介绍

作者：（意大利）格涅斯（Stefania Gnesi） （意大利）玛格丽特（Tiziana Margaria） 译者：靳添絮 连晓峰

文摘

版权页：



时间模型的。该语义用于离散时间进程代数的设定。在由ProRail资助的后续项目中，来自阿姆斯特丹工人国际委员会（CWI）的研究人员设计了一种名为LARIS的文本形式EURIS，旨在提高图形化LSC的清晰度。EURIS规范的验证工作正在阿姆斯特丹的CWl进行。另外，还实现了EURIS到CRL的编译器原型，并在cRL工具集的帮助下，解决了荷兰Woerden—Harmelen车站的EURIS规范验证。因此，可提供该联锁系统的状态空间符号版本用于分析。利用CRL工具集可实现一个（更小的）虚构火车站的EURIS规范的正确性验证。
有关Woerden—Harmelen的验证工作使得在形式化验证领域取得一些进展。即由于该车站联锁系统的状态空间太大，因此必须利用CRL工具集来实现新的验证方法，以应付如此大的状态空间。这些新的验证方法基于部分降阶法、分布式状态空间生成法以及分布式状态空间小化。
EURIS的所有权已经从ProRail转卖给西门子公司，以保证更加强大的商业支持和工具开发。目前，EURIS是西门子公司GRACE工具集的核心。
4.6 小结
随着欧洲共同体强制推行开放市场，铁路发展在过去的几十年内发生了巨大变化，但可以看到形式化方法在铁路信号中的应用发展历史并未脱离铁路的发展历史。其中，见证了向基于行为、状态机的形式化转变，以及商业化工具越来越多地关注向形式化支持的转变。具有仿真和模型校验规范并生成代码的工具将会产生附加值。但是，这对于主要从事软件生产或微型设备的小公司来说，可能由于太过于昂贵而望而却步。在得到一个令人满意的解决方案之前，还将有一段很长的时间。
规范和验证的形式化方法正逐步平稳地得到工业环境下的认可和应用：在学术界已有许多符号、方法和（原型）工具，然而，在工具稳定性、规范文档和用户支持方面尚缺乏工业实际应用，另一方面，在工业中也出现一些具有技术含量的方法和工具。尽管在实际应用中利用这些（得到工业应用）工具来实现复杂硬实时系统的全面验证仍是不可行的，但是验证技术正得到快速发展。

序言