2基于UML机制的列控系统需求规范建模方法介绍
规范是系统开发的起点和基础，系统规范的缺陷将给项目成功带来极大的风险。对于列控系统这样安全荀求系统而言，系统需求规范中的任何缺陷都有可能由潜在的风险演变成系统失效从而导致安全事故的发生。因此，以列控系统需求规范为研究对象，本章将对其所体现的混成特性建模需求进行分析，研究UML扩展机制，充分挖掘UML的图形功能，设计面向列控系统需求规范的混成UML概要文件，使之能够包含更多的内容与信息去准确地刻画列控系统的混成特性，最后介绍建模所选择的工具。
2.1列控系统需求规范建模的需求分析
针对列控领域的建模需求扩展UML，首先要为其提供刻画连续动态行为的能力，扩展后的UML类似于一种特定领域语言(Domain-Specific Language)。这种做法在其他领域有成功的先例，例如，对于实时和嵌入式系统，OMG发布了一个标准的 UML 扩展规范 MARTE[41](UML Profile for Modeling and Analysis of Real-Timeand Embedded Systems)。其次，这种扩展应具有层次化和可组合的特性，基于混成自动机的底层语义，使得在其上进行形式推理和验证成为可能。针对列控系统混成特性的建模需通过带有连续变量的微分表达式刻画系统中连续的物理过程以及保持这些过程的微分动态约束条件；以及以不变集或信号事件等为条件的状态迁移刻画离散变化过程。面向列控领域UML建模的难点在于创建能够刻画列控领域混成特性的UML概要文件。具体对刻画列控领域混成特性的所有元素(已存在的元类元素和扩展元素)进行分析，可根据元素间的扩展与被扩展关系、扩展元素之间的应用关系，按功能分为六个包(见图2-1):基础包(Basicspackage),数据类型包(Types package)，数据包(Data package)，表达式包(Expressionspackage)，通信包(Communications package)，扩展类和扩展状态机包(Modes andAgents package)。
2.2 UML扩展机制
UML概要文件主要由原型组成，一个原型定义了与其关联的UML类(即元对象类)、这个类的属性及这个原型元素与其它元素如何进行关联的约束条件。在概要文件中对原型进行描述，主要依照三种扩展机制：
(1)标称值(Tagged Value)标记值是对一个特性的显式定义，是一种用于指定模型元素性质的机制。它由一个标记字符串和一个值字符串组成，可以连接到任何元素上，可以给一个元素增加一些新的语义。标记值已成为一种用来提高模型质量以提供附加信息的有效方法。
(2)约束(Constrains)约束是指作用于一个或多个元素之上的语义条件或限制，即使用一个表达式把约束应用于元素上。它是用大括弧内的字符串表达式来表示的，可以附加在依赖、注释等元素上以表示约束和关系，因此可以用来对模型元素进行语义上的限制。在定义一个约束时，应该给出该用户自定义约束将应用于哪一种元素以及对相关元素的语义影响力。在UML2.0中，对象约束语言(Object Constraint Language.简称OCL)提供了一种标准方法来明确表达UML2.0模型上的约束。
(3)构造型(Stereotype)构造型是最复杂的扩展机制，这种机制是基于一个己存在的模型元素定义一种新的模型元素，通过构造型来标识那些可以被重用而不需要由转换生成的元素。一方面，新的模型元素只是已有模型元素的子类，通过泛化关系继承了其元对象类的形式和特征；另一方面，由于添加了额外的语义，新的模型元素实现了对其基类的扩展。构造型是原型的直观表现形式，通常有两种：普通构造型(简称构造型)和枚举构造型(简称枚举)。对于表现形式为构造型的原型，至少应该具有1个(可有多个)与它关联的元对象类。本文主要通过向构造型加入属性的方式来对元类元素进行结构上的扩展，或通过加注释的形式进行静态语义的扩展，这种概要文件扩展机制，使得扩展的定义更容易被理解，扩展元素之间的相互关系、以及扩展元素与UML模型之间的应用关系都更加清晰、准确而完整。
2基于UML扩展机制的列控系统.........................................9
2.1列控系统需求规范建模的.....................................9
2.2UML扩展机制.....................................10
2.3面向列控系统需求规范的.....................................11
2.4RSA建模工具.....................................18
3列控系统需求规范模型的.....................................21
3.1列控系统需求规范分析.....................................21
3.2列控系统需求模型验证分析.....................................22
3.3列控系统需求规范验证支持.....................................23
3.4列控系统需求规范验证支持工具.....................................25
3.5列控系统需求规范验证支持工具.....................................37
5结论
我国轨道交通正处于高速发展时期，干线列车提速、客运专线、高速铁路建设需要安装使用列车运行控制系统来确保列车运行安全。对于列控系统而言，离散的计算过程和连续的物理过程在开放环境下持续交互并深度融合，为其建模和验证工作增添了不少难度。以列控系统需求规范为研宄对象，一方面，需要提出一种合理的框架结构以对其混成特性进行建模。统一建模语言(UML)作为一种广泛使用的面向对象的可视化统一建模语言，己被应用到不同的领域，但混成特性的描述己经远远超出了这种建模语言本身的能力范围。另一方面，对系统进行验证的需求来看，形式化方法为规范验证提供了一条重要的解决途径，供研宄人员使^的形式化验证工具种类繁多，可集成几种常用的形式化验证工具，支持列控系统规范的验证分析工作。因此，本文针对列控系统需求规范，着眼于运用UML自身所提供的扩展机制研宄一种有效的建模方法；并在Eclipse平台上完成了一个验证支持工具的软件原型开发。重点包括了如下的几个方面：
(1)准备工作阶段，阐述了工作的选题目的和立体意义，概述了CTCS-3级列控系统的系统结构，了解国内外形式化建模验证方法的研究现状，并借鉴国内外已有的形式化验证工具集成平台的开发经验。
(2)建模阶段，从列控系统需求规范建模的需求着手进行分析，针对列控系统的混成特性，设计了面向列控系统需求规范的混成UML概要文件。
(3)验证阶段，在阐述列控系统需求规范分析体系结构的基础上，重点分析了验证阶段的功能需求，为达到对列控系统需求规范进行验证分析的目的，集成两个常用的形式化验证工具，完成验证支持工具的原型开发。
