基于UML及属性的需求分析方法在列控系统需求规范中的应用

程瑞军 赵 林 何丽芸

程瑞军:北京交通大学电子信息工程学院 硕士研究生 100044北京

赵 林:北京交通大学轨道交通控制与安全国家重点实验室讲师 100044北京

何丽芸:北京交通大学电子信息工程学院 硕士研究生 100044北京

CTCS-3级列控系统需求规范，是CTCS-3级列控系统开发的起点和基础，是确保列控系统高效安全运行的关键环节。列控系统是典型的复杂安全苛求系统，根据国际标准IEC61508-1，对高安全系统 (安全完善度等级4级)强烈推荐使用形式化方法进行分析。

形式化方法采用严格的数学语言，具有精确的数学语义，适合于软、硬件系统的描述、开发和验证。国内外学者虽然提出了许多有用的形式化方法和模型检验工具，对列控领域的形式化方法进行归纳，然而对于工程人员来说，由于对大多数的形式化语言和验证技术并不熟悉且难以理解，限制了形式化方法在工业界的广泛应用。针对这一现状，需要运用一种简便的方法来对系统进行建模。UML是一种半形式化的建模语言，目前已被视为事实上的工业标准。同时，PSL(Property Specification Language)是一种易于读写、语法精简、语义严格清晰的硬件设计属性说明语言，为建立形式化模型提供了简单的途径，并可运用RATSY(Requirements Analysis Tool with Synthesis)对PSL模型进行形式化验证。

因此，采用基于属性的分析方法，不仅简化了建模过程，而且在自然语言描述的规范与PSL模型之间建立了联系，保证模型对需求规范的覆盖能力。

1 基于属性的需求分析方法

基于属性的分析方法是个不断迭代的过程。图1描述了基于属性的分析方法流程。主要的分析步骤简述如下。

第1步，建立规范中对应场景的UML模型。

第2步，根据转换规则，将UML模型转换为PSL形式化规范。该属性规范是系统的抽象可执行模型，允许在不考虑实现细节的情况下，使用该模型进行仿真、调试和验证。

第3步，验证该形式化模型是否能实现，即是否存在可实现的系统。如果是可实现的，则转到第4步;若为不可实现，需运用RATSY工具调试并修改该PSL模型，通过反例对错误进行定位和修改，最终得到可实现的规范模型。

第4步，当需求可实现时，通过模型检验和仿真的方法进行验证，验证该模型是否具有某些属性。若形式化需求不满足某个属性，就会得到一个反例。

运用上述分析方法，最终将得到PSL描述需求规范模型。系统可用一个四元组表示:

Y= ＜ S，E，A，G ＞。

其中，S和E是变量的2个不相交集，S代表系统变量 (受系统控制的变量)，E代表环境变量(受环境控制的变量)。需求分为保证需求和假定需求，保证需求用G表示，是关于系统变量的PSL属性集;假定需求用A表示，是关于环境变量的PSL属性集。

图1 基于属性的分析流程

RATSY是一种基于属性的需求分析工具，为工程人员提供了仿真、验证和调试的环境。以下举例说明基于属性的分析方法在列控领域中的应用。

2 基于属性的分析方法在需求规范验证中的应用

列车运行控制系统由地面设备和车载设备构成，用于控制列车运行速度，保证行车安全，提高运输能力。由于包括有大量的子系统且功能复杂，正确地开发列控系统是很困难且容易出错的。在开发过程中，正确理解并建立系统需求规范是首要问题。为了尽早发现规范中的漏洞，借助计算机辅助分析手段建立形式化的需求规范是一种有效途径。以下运用UML和RATSY对CTCS-3列控系统需求规范中的模式转换部分进行了建模和验证。

2.1 模式转换

模式转换部分的规范描述了CTCS-3级列控系统的车载设备在不同工作环境下的工作模式及转换过程。在配置有CTCS-3级基础设备的区段，且不考虑故障的情况下，车载设备共有9种工作模式，分别为完全监控模式 (Full Supervision，FS)、目视行车模式 (On Sight，OS)、引导模式 (Call On，CO)、调车模式 (Shunting，SH)、隔离模式(Isolation，IS)、待机模式 (Stand By，SB)、休眠模式 (Sleeping，SL)、冒进防护模式 (Trip，TR)和冒进后防护模式 (Post Trip，PT)。各模式的具体使用环境及主要功能参考文献。

2.2 模式转换的PSL建模过程

2.2.1 建立模式转换的UML模型

模式转换中，车载设备需同无线闭塞中心、列车、应答器等进行信息交互。采用面向对象的方法将CTCS-3级列控系统中的实体抽象为几个相互关联的类，分别为车载设备类 (OBE)、司机类(Driver)、列车类 (Train)、无线闭塞中心类(RBC)和应答器类 (Balise)。由于人机界面只起接口作用，与模式转换的切换过程无关，在此不作考虑。

图2给出了模式转换的类图，并对每个类的属性、操作进行了举例说明。图2中关联线所标示的数字表明关联中的数量关系，例如，一列车上装有2个车载设备。图2中属性和操作与规范的对应关系见表1。

根据需求规范的内容，将车载设备的工作模式表示为工作状态。建立模式转换的UML状态转移图，如图3所示。图3表示了列控系统车载设备工作状态的切换过程。状态迁移条件使用不同的标号进行表示，例如，P2t20，P1t1等。其中P2，P1等表示该转移条件的优先级，数字越小则迁移优先级越高。t20，t1等表示迁移条件的名称，条件的具体内容可以参见文献，在此不再赘述。

图2 模式转换的类图

图3 模式转换部分的状态迁移图

表1 图2中类属性和操作与规范对应关系表

2.2.2 定义由UML模型到PSL模型的转换规则

1．定义模式转换场景涉及的环境变量和系统变量。由于模式转换可研究车载设备的各工作模式的切换过程，因此以车载设备的工作模式为系统变量，输入车载的信息及操作为环境变量建立模型。根据PSL的特点，引入消息机制，使用布尔型数据代替整型及字符串型数据。以变量BaliseID(应答器号)为例，需求规范验证过程关注的是应答器号是否在列车的应答器列表中，而该变量的具体取值对验证结果并不产生影响。因此使用事件 IN_ListOfBalises进行替换。IN_ListOfBalises的值为0，表示该应答器不在列车的应答器列表中;值为1，表示在列车的应答器列表中。对类的操作进行类似变换，如 IsolateBrake()，引入布尔型的事件Iso_Brake。

2．定义系统的初始工作状态。车载设备上电后应进行自检和外部设备测试，自检和测试通过后自动进入待机模式。

A1:T_stop＆＆ OBE_awake＆＆ !Iso_brake

G1:SB＆＆!SH ＆＆!FS＆＆!OS＆＆!CO＆＆!SL＆＆!TR＆＆!PT＆＆!IS

3．约束环境事件和系统变量。对互斥的事件进行约束，如隔离制动和恢复制动的操作不能同时发生，由PSL定义为A2:never(Iso_brake＆＆Recover_brake)。对车载工作状态进行约束，如不考虑故障情况，车载设备工作在CTCS-3级时，共有9个工作模式，在某一时刻CTCS-3级列控系统只能处于一种工作模式。

PSL描述为:

G2:(always(SB＜－＞!(SH||FS||OS||CO||SL||TR||PT||IS)))

G3:(always(SH＜－＞!(SB||FS||OS||CO||SL||TR||PT||IS)))等。

4．定义状态迁移。根据UML状态图，将模式转换过程转换为PSL描述，并作为约束集S的组成部分。例如，由隔离模式转换到待机模式:

G4:always(T_stop＆＆Recover_brake＆＆OBE_awake＆＆IS－ ＞next(SB))

5．待验证性质。由PSL描述系统待验证的属性。如车载设备从待机模式 (SB)到调车模式(SH)的转移特性，由PSL描述为:

P1:eventually!(SB＆＆next(SH))。

2.2.3 建立PSL模型

根据2.2.2的转换规则，初步得到一个交互式的可执行模型Y=＜S，E，A，G ＞，其中各集合对应的含义为:

S={SB，SH，FS，OS，……:boolean};

E={Iso_brake，T_stop，……:boolean};

A={A1，A2，……};

G={G1，G2，G3，G4，……}。

2.3 对PSL形式化规范进行调试和验证

2.3.1 对PSL模型进行调试

RATSY工具封装了NuSMV，以便对可实现的PSL模型进行验证，对不可实现的PSL模型进行调试。以一个反例来介绍调试过程。根据实现性的概念，RATSY仅保留集合A和S中与可实现相关的约束集G2、G3、G5、G6等，并给出了反例 (如图4)。在step1，系统初始化工作模式为待机模式(SB);在step2，E_Brake(车载接收到紧急停车信息)、Iso_brake(隔离车载制动功能)和T_stop(列车停车)同时满足，根据G5车载设备应切换至调车模式SH，根据G6车载设备应切换至完全监控模式FS。但由G2、G3等约束知车载设备只能处于一种工作模式，故G2、G5和G6规范之间存在冲突。考虑到实际情况，当车载设备处于待机模式时，RBC不能既给车载发送行车许可MA，同时又允许车载进入调车模式。因此需加入对环境变量的约束A3:never(RBC_per_SH＆＆Tdata_MA)。验证修正后的规范是可实现的。最后需在需求规范中写入该条信息，即RBC不能同时给车载发送行车许可和允许调车命令。

图4 GAME中的反例

2.3.2 模式转换特性的验证

对CTCS-3级列控系统需求规范进行验证，验证所建立的模型是否具有某些属性。对于断言类的属性 (用As标记)，若不满足会给出反例;对于可能性属性 (用P标记)，若满足则给出仿真结果。由于涉及系统的所有模式，验证内容较多，因此仅对验证过程举例介绍。

1．可达性验证。例如，P1:eventually!(SH)，该属性表示系统可以从其他状态到达调车模式 (SH)状态。验证结果为真，存在一条到达调车模式的路径，调车模式 (SH)可达。

2．转移性验证。例如，P2:eventually!(SB＆＆next(SH))，表示车载设备从待机模式(SB)可以经过1个转换步骤切换至调车模式(SH)状态。验证结果为真，并得到一条满足该属性的路径 (如图5所示)，其中Step1为初始化状态，系统从Step2开始运行，经过一个转换步骤到SH模式。因此，系统由SB模式到SH模式具有转移性。

图5 验证eventually!(SB＆＆next(SH))的仿真结果

3．死锁性验证。例如，As1:never(eventually!(always(SH)))，该属性表示系统不会在很长一段时间内停留在调车模式。验证结果为假，表明系统可能在很长一段时间内处于调车模式，会出现死锁，需要添加新的需求。车载工作于调车模式且列车在停车状态下，司机可通过再次按压调车键退出调车模式转入SB模式。编辑该需求的Büchi自动机 (如图6所示，其中Init为Büchi自动机的初始状态)，并通过RATSY转换成PSL公式，添加到原PSL模型中。重新进行验证，验证结果满足As1属性的要求。

本文运用基于属性的需求分析方法，对CTCS-3级列控系统需求规范中的模式转换部分进行形式化验证。采用UML与PSL相结合的方法，利用RATSY对PSL模型进行相关属性的验证，通过反例对错误进行定位和修改。验证过程表明基于属性的分析方法适用于CTCS-3级列控系统需求规范的验证。该方法简便易行，对于初步编写规范及对原有系统规范进行更新升级的工作具有重要的意义。

图6 编辑Büchi自动机作为新需求

［1］ 中华人民共和国铁道部．CTCS-3级列控系统系统需求规范(SRS)［M］ ．北京:中国铁道出版社，2009．

［2］ BOWEN J P．Formal Methods in Safety－Critical Standards［C］ //Software Engineering Standards Symposium．Brighton:IEEE Computer Society Press，1993:168－177．

［3］ 古天龙．软件开发的形式化方法［M］ ．北京:高等教育出版社，2005:15－20．

［4］ 曹源，唐涛，徐田华，等．形式化方法在列车运行控制系统中的应用［J］ ．交通运输工程学报，2010，10(1):112－126．