刘 磊
(中国铁道科学研究院集团有限公司通信信号研究所,北京 100081)
CTCS-3级列控系统(Chinese Train Control System Level 3)是一个将先进的计算机技术、通信技术以及控制技术融合为一体的复杂安全苛求系统。国际标准IEC61508-1和欧洲铁道行业EN50129均强烈推荐利用形式化方法对列控系统进行分析[1-2], 因此针对CTCS-3级列控系统进行建模和形式化分析对于完善系统功能和提高系统安全性显得十分必要。
国内针对CTCS-3级列控系统规范建模和形式化方法进行了一系列的探索和研究,并取得大量成果[3-10]。文献[8-10]采用能够刻画列控系统混成特性的Hybrid UML(HUML)对系统规范进行半形式化建模,再利用模型转化手段将其转化为某一具体的形式化模型,最后利用模型检验的形式化分析方法进行验证,此方法便于使用计算机辅助工具,易于操作且自动化程度较高,在列控系统建模和形式化分析领域中得到广泛应用。但是,此方法针对系统安全性分析均是在形式化建模阶段进行,如建立故障模型、使用故障注入手段等,需要运用形式化复杂的数学理论,不利于在工业界推广。
本文根据UML扩展机制,对HUML进行安全特性扩展,对列控系统的安全需求和安全特性进行描述,进行半形式化模型安全设计,以半形式化模型为安全分析起点,从而达到降低形式化安全分析带来的复杂度,便于在工业界推广的效果。
统一建模语言 (Unified Modeling Language,UML)是一种定义良好、易于表达,功能强大且普遍适用的图形化、半形式化建模语言[11]。为了保持良好的应用性,且能够描述不同领域的特性和规则,UML底层设计了扩展机制[12],UML的扩展机制允许使用者设计UML概要文件(Profile),使用构造型(Stereotype)、标记值(Tagged Value)和约束(Constraint)三种扩展机制自定义不同领域内的元素[13]。
HUML是利用UML的概要文件扩展机制,构造出的能够对混成系统建模的半形式化建模语言。该语言能够对列控系统既包含离散时间变量又包含连续时间变量的混成性进行建模。HUML按照功能结构划分为6个包,基础包(Basics),数据类型包(Types),数据包(Data),表达式包(Expressions),通信包(Communi-cations)以及扩展类和扩展状态机包(Modes and Agents)[14],如图1所示。
图1 HUML元素模型包的关系
HUML元模型的这种包结构描述了模型的组成元素和之间的抽象语法。基础包定义了建模中以抽象类存在的基本建模概念。数据类型包定义了基本数据类型。表达式包扩展定义了约束(Constraint)和表达式(Expression)的形式。扩展类和扩展状态机包是模型的核心,定义了与扩展类(Agent)和扩展状态机(Mode)相关的所有元素。扩展类创建了系统的框架结构,扩展状态机描述了系统的动态交互行为[15]。
IBM Rational Software Architect(RSA)是一种应用广泛的基于UML的图形化建模工具,用户可以用组件化和可视化的方式为复杂系统进行建模,本文中将其作为HUML以及HUML安全特性扩展的原型软件工具。
安全特性是指与系统安全性相关的一些元素,包括影响系统安全的相关元素和保障系统安全的相关元素。其中,前者是指系统在运行过程中可能出现的故障,以及用以表述这些故障的成分,如类型、苛求程度等。后者是指系统在设计过程中应当采取的用以保障系统安全或达到一定安全完善度等级的措施、性能指标等。对HUML进行扩展的主要目的就是期望HUML能够对这些元素进行描述。
在进行HUML扩展时,可将安全特性相关元素放在一个独立的安全特性包中。安全特性包定义了安全特性相关元素,以及各个元素之间的关系。这样可以在现有的模型上叠加安全特性元素而无需改变原有的模型元素。安全特性包中的元素由HUML模型元素扩展而来,将HUML的模型元素作为安全特性元素的扩展基础。可以在不改变HUML模型元素的基础上增加安全特性元素,令新的HUML既可以进行混成特性建模,又可以包含安全特性元素。
将安全特性包加入HUML元模型中,构成新的HUML元模型。根据各个元素的类别不同,可以将所有的元素分成7个不同的包,如图2所示。
图2 安全特性扩展后的HUML元模型
图2描述了扩展后的HUML元模型中各个元素包的关系,在新的元模型中,安全特性包仅与基础包、类型包、表达式包以及扩展类和扩展状态机包有关。安全特性包中的元素及其之间的关系,如图3所示。
图3中各元素的含义如下。
(1)故障(Fault):故障描述了系统在运行过程中可能会出现的异常情况。根据CTCS-3级列控系统的不同组成部分,可细分为人机接口故障(MMI_Fault)、列车接口故障(TI_Fault)、车载计算机故障(KERNEL_Fault)、测速单元故障(ODO_Fault)、无线闭塞中心故障(RBC_Fault)以及与信息传输相关的设备功能故障(TRANS_Fault)等。
图3 安全特性包中元素及关系
(2)故障类型(Fault Type):故障类型描述了具体的故障所属类型,根据故障所涉及到的不同功能,具体可分为信息重复(Repetition),功能或信息不合时宜的出现(Insertion),信息顺序错误(Resequence),信息丢失(Del-etion),延迟(Delay),功能错误或数据错误(Corruption),信息错误(Masquerade),功能缺失(Absent),功能实时时机错误(Timing),实施错误的功能(Incorrect),测速或测距偏大(More),测速或测距偏小(Less)等。
(3)苛求度(Criticality):苛求度描述了故障所涉及的功能或数据对于列控系统安全的影响程度。根据安全分析的结果,将故障涉及的功能或数据分为三类:安全苛求的(Safety Critical)、安全相关的(Safety Related)和安全无关的(No Safety Related)。
(4)缓解措施(Fault Mitigation):缓解措施是针对安全苛求或者安全相关的失效功能而提出的缓解办法,主要目的是降低该功能失效的频率或者失效带来的影响。当然,不是所有的功能都具有缓解措施,譬如有些系统的固有的核心功能一旦故障,是无法进行缓解的(不包括冗余设计措施)。
(5)危险容忍率(THR):危险容忍率(Tolerable Hazard Rate, THR)是指在满足一定的安全完善度等级前提下,允许危险发生的最大频率。危险容忍率属于系统级指标,根据系统的组成以及安全分析的结果,可对各子系统进行THR的分配。
(6)安全性策略(Safety Policy):上述危险容忍率分配以及缓解措施的制定共同构成用于保障系统安全的安全性策略。
面向列控系统安全特性对HUML进行扩展,本质就是在HUML模型元素的基础上进行安全特性扩展,通过建立概要文件,创建构造型的方式,对需要扩展的元素进行定义。创建的概要文件及定义的元素如表1所示。
表1 概要文件及构造型
下面对表1中概要文件各部分进行详细介绍。
HUML元模型中数据类型包定义了所用数据类型,数据类型包中包括元类元素枚举类型(Enumer-ation),安全特性包中故障类型(Fault Type),苛求度(Criticality)则是元类元素枚举类型(Enumeration)的扩展,在RSA工具中,可通过图4所示的构造型扩展实现。
图4 数据类型的构造型实现
HUML元模型中表达式包定义了表达式和约束,安全元素包中所用的危险容忍率(THR)是对HUML元类元素表达式的扩展,缓解措施(Fault Mitigation)是HUML元类元素约束的扩展,在RSA工具中,可通过下述构造型扩展实现,如图5所示。
图5 表达式及约束的构造型实现
故障(Fault)作为安全元素的核心,属于元类元素(信号)的扩展,为了简化RSA实现过程,以信号事件的形式表示功能故障事件。因为故障不会像信号一样存在发出和接受的执行动作,因此采用布尔型的取值规则表示故障的发生与否,同时会触发状态图的迁移。由于系统存在不同的功能单元,其故障表示方式也不同,因此可以根据系统特性,对Fault进行细化,综合两方面,在RSA工具中,可通过图6所示构造型扩展实现。
图6 Fault构造型实现
扩展类和扩展状态机包中描述了前述的危险容忍率(THR)、故障(Fault)等元素与类(Agent)的关系,即描述了如何在建模过程中体现这些安全特性元素。
图7给出了Agent元素与安全特性元素的关系,即类具有相应的故障事件,构造安全参数(safepara)代表安全完善度等级,根据相应的安全完善度等级会对该类进行THR的分配。其中,THR分配过程会以参数表达式的形式存在。RSA工具中,可通过图7所示的构造型扩展实现。
图7 Agent构造型实现
图8 车载设备建模示意
以CTCS-3级列控系统车载设备为例,建立包含安全特性的类图,如图8所示,图中的车载设备类(OBE),包含几个故障事件,例如,车载设备无法施加制动 (F_NotBrake)具有类型以及苛求度的特征;车载设备位置错误(F_IncorrectDistance),属于功能错误(corruption)类型、安全相关(SafetyRelated)的故障。同时,通过参数表达式的形式给出了THR的分配信息。对于可缓解的故障事件,会存在《Fault Mitigation》的缓解措施,例如车载设备位置错误(F_Incorrect Distance)存在应答器链接反应(linking reaction)的缓解措施。
本文基于UML的扩展机制,提出一种面向列控系统安全特性的HUML扩展方法,扩展后的HUML能够在建模过程中对列控系统的安全特性进行描述。此方法弥足了HUML模型无法直接刻画列控系统安全特性的不足,为列控系统建模和形式化分析提供了一条新的思路。由于RSA软件的一些限制,有些设计没有完全实现,仅是通过现有元素进行代替。为此,可进一步研究UML的扩展机制,在现有RSA有限表达能力的情况下实现表达能力更好的概要文件。