作者：唐涛//徐田华//赵林
页数：206
出版社：中国铁道出版社
出版日期：2010
ISBN：9787113114602
电子书格式：pdf/epub/txt
内容简介
本书主要介绍了实现列控系统需求规范的严格建模与验证所必须的理论、方法和关键技术，内容包括现代列车运行控制系统的特点和相关标准规范、系统规范的严格建模与验证体系、模型检验相关基础知识、需求规范的管理和追踪、列控领域的uml建模以及针对ctcs－3系统规范展开的实例分析。
本书内容丰富，注重背景，可以作为研究生、教师以及轨道交通控制领域相关的科研人员了解列控系统规范的建模与验证的基本思想和方法的参考书。
相关资料
插图：（2）属性一个类可以有一个或多个属性，或者没有属性。属性用来描述该类的对象所具有的静态特征。类的属性分为两类：一类属性代表的状态可以被其他对象存取；另一类属性代表的是对象的内部状态，它们只能够被类的操作所存取。属性必须命名，以区别类的其他属性。当一个类的属性被完整地定义后，它的任何一个对象的状态都被这些属性的特定取值所决定。在需求分析阶段，只抽取那些系统中需要使用的特征作为类的属性。正如变量有类型一样，属性也是有类型的，属性的类型反映属性的种类。比如，属性的类型可以是整型、实型、布尔型、枚举型等基本类型。除了基本类型外，属性的类型可以是程序设计能够提供的任何一种类型。同时，属性可以定义不同的可见性，利用可见性可以控制外部事件对类中属性的操作方式。而且，当类的一个对象被创建，它的各个属性就开始有特定的状态。对象的状态在对象参与交互的过程中会发生变化，有时对象的初始状态对此对象参与的交互是有意义的。这时，有必要在对象的类中定义其对象的属性的初始值。此外，关于类的属性，还涉及多重性、约束特性、类属性等相关性质，在此不一一进行介绍。UML规定类属性的语法格式为：[可见性]属性名：类型[=初值][{约束特性}]其中“[]”中的部分是可选的。说明其中除了属性名和类型名是一定要有的，其他部分可根据需要可有可无。
本书特色
《列车运行控制系统规范建模与验证》：国家自然科学基金——铁道联合重点项目(60634010)资助
目录
第一节 轨道交通列控系统发展趋势
第二节 列控系统规范验证的意义
第三节 列控系统规范的建模验证方法
第四节 列控系统规范的严格建模与验证体系
本章参考文献
第二章 系统需求规范建模与验证基础
第一节 系统需求规范
第二节 验证和确认的概念
第三节 系统开发模型
第四节 uml基础知识
第五节 符号模型检验
本章参考文献
第三章 列控系统的需求规范验证内容与体系
第一节 列控系统需求规范验证内容
第二节 列控系统需求规范验证方法体系
第三节 列控系统需求规范验证流程
本章参考文献
第四章 需求规范的管理
第一节 需求规范管理的概念与意义
第二节 需求规范管理的任务
第三节 需求规范管理流程
本章参考文献
第五章 列控系统的uml建模
第一节 列控系统uml模型库
第二节 列控系统规范的uml模型
本章参考文献
第六章 列控系统的形式化验证
第一节 列控系统规范uml模型到nusmv的转换
第二节 列控系统模型的约简
第三节 列控系统规范验证结果分析
本章参考文献
第七章 实例分析
第一节 背景介绍
第二节 需求规范管理
第三节 ctcs一3级系统需求规范的uml建模
第四节 nusmv转换
第五节 验证结果分析
本章参考文献
附录a nusmv系统简介
附录b 系统开发模型介绍
节选
《列车运行控制系统规范建模与验证》主要介绍了实现列控系统需求规范的严格建模与验证所必须的理论、方法和关键技术，内容包括现代列车运行控制系统的特点和相关标准规范、系统规范的严格建模与验证体系、模型检验相关基础知识、需求规范的管理和追踪、列控领域的UML建模以及针对CTCS－3系统规范展开的实例分析。《列车运行控制系统规范建模与验证》内容丰富，注重背景，可以作为研究生、教师以及轨道交通控制领域相关的科研人员了解列控系统规范的建模与验证的基本思想和方法的参考书。
