列车运行控制系统规范建模与验证 本书特色

《列车运行控制系统规范建模与验证》：国家自然科学基金——铁道联合重点项目(60634010)资助

列车运行控制系统规范建模与验证 内容简介

本书主要介绍了实现列控系统需求规范的严格建模与验证所必须的理论、方法和关键技术，内容包括现代列车运行控制系统的特点和相关标准规范、系统规范的严格建模与验证体系、模型检验相关基础知识、需求规范的管理和追踪、列控领域的uml建模以及针对ctcs－3系统规范展开的实例分析。
本书内容丰富，注重背景，可以作为研究生、教师以及轨道交通控制领域相关的科研人员了解列控系统规范的建模与验证的基本思想和方法的参考书。

列车运行控制系统规范建模与验证 目录

列车运行控制系统规范建模与验证 节选

《列车运行控制系统规范建模与验证》主要介绍了实现列控系统需求规范的严格建模与验证所必须的理论、方法和关键技术，内容包括现代列车运行控制系统的特点和相关标准规范、系统规范的严格建模与验证体系、模型检验相关基础知识、需求规范的管理和追踪、列控领域的UML建模以及针对CTCS－3系统规范展开的实例分析。《列车运行控制系统规范建模与验证》内容丰富，注重背景，可以作为研究生、教师以及轨道交通控制领域相关的科研人员了解列控系统规范的建模与验证的基本思想和方法的参考书。

列车运行控制系统规范建模与验证 相关资料

插图：（2）属性一个类可以有一个或多个属性，或者没有属性。属性用来描述该类的对象所具有的静态特征。类的属性分为两类：一类属性代表的状态可以被其他对象存取；另一类属性代表的是对象的内部状态，它们只能够被类的操作所存取。属性必须命名，以区别类的其他属性。当一个类的属性被完整地定义后，它的任何一个对象的状态都被这些属性的特定取值所决定。在需求分析阶段，只抽取那些系统中需要使用的特征作为类的属性。正如变量有类型一样，属性也是有类型的，属性的类型反映属性的种类。比如，属性的类型可以是整型、实型、布尔型、枚举型等基本类型。除了基本类型外，属性的类型可以是程序设计能够提供的任何一种类型。同时，属性可以定义不同的可见性，利用可见性可以控制外部事件对类中属性的操作方式。而且，当类的一个对象被创建，它的各个属性就开始有特定的状态。对象的状态在对象参与交互的过程中会发生变化，有时对象的初始状态对此对象参与的交互是有意义的。这时，有必要在对象的类中定义其对象的属性的初始值。此外，关于类的属性，还涉及多重性、约束特性、类属性等相关性质，在此不一一进行介绍。UML规定类属性的语法格式为：[可见性]属性名：类型[=初值][{约束特性}]其中“[]”中的部分是可选的。说明其中除了属性名和类型名是一定要有的，其他部分可根据需要可有可无。