基于MSC与UPPAAL的区域控制器切换场景建模与验证

杨 璐，陈永刚

(兰州交通大学自动化与电气工程学院，兰州 730070)

基于通信的列车运行控制系统(Communication Based Train Control， CBTC)用于控制城市轨道交通列车的运行，是保证列车安全、高效运行的系统，区域控制子系统作为其关键的轨旁设备，主要实现为辖区内的列车计算移动授权(Moving Authorization， MA)、完成边界切换等功能[1-2]。如果ZC子系统控制逻辑存在潜在缺陷，很可能导致CBTC系统在运行中失效，造成人员伤亡或重大财产损失等灾难性后果[3]。为了保证列车安全运行、降低事故发生率、需要高可靠性、高安全性的列车运行控制系统作为保障[4]。ZC切换作为CBTC系统的重要场景，是保证行车安全的基础，因而，针对ZC边界切换功能安全性的验证就显得尤为重要。

目前，已有许多学者对列控系统的安全性和实时性进行了大量的研究，如刘金涛博士采用基于微分动态逻辑理论的推理证明方式对RBC子系统进行了建模验证，采用大量的公式推理，验证过程繁琐复杂[5]。张友兵采用有色Petri网和故障树实现了对RBC两种切换方式的建模，并对切换成功率进行了评估，但没有实现有效的验证[6]。黄友能采用混成自动机理论对城市轨道交通ZC子系统的混成性进行了研究，但组合片段转换过程复杂易出错[7]。本文采用半形式化方法MSC和形式化方法UPPAAL相结合的方法对ZC切换场景进行研究，建立ZC切换过程的MSC模型，将其转换为时间自动机模型，采用验证工具UPPAAL对其安全性和受限活性进行验证。

1 ZC切换过程分析

当列车从移交ZC辖区进入接管ZC辖区时，控制列车运行的区域控制器应从移交ZC切换至接管ZC，切换过程分为以下4步。

(1)列车在移交ZC区域内运行，当列车接近分界点P，即列车收到以分界点P为终点的MA时，移交ZC与接管ZC建立通信会话，触发边界切换功能，如图1所示。

图1 边界切换触发控制示意

(2) 如图2所示，当移交ZC与接管ZC通信成功后，移交ZC计算MA1，同时向接管ZC发送切换预告信息并为列车请求接管ZC范围内的进路，进路排出以后接管ZC将MA2发送给移交ZC，移交ZC将混合后的MixedMA发送给列车，控制列车运行。

图2 MA延伸至接管ZC时切换控制示意

(3) 如图3所示，当列车前端越过分界点P时，车载系统与接管ZC之间建立通信连接，车载系统与接管ZC连接成功以后，车载系统向接管ZC发送登录申请，接管ZC发送数据库版本信息，列车向接管ZC发送登录确认信息后登录成功。

图3 车头越过边界点时边界切换控制示意

(4) 如图4所示，当列车车尾越过分界点P后，列车向接管ZC发送受控申请，向移交ZC发送注销申请，当列车收到接管ZC发送的控制列车的信息后，移交ZC向列车发送注销确认信息，列车根据接管ZC发送的控制信息控制列车正常运行，至此，整个边界切换过程结束。

图4 车尾越过边界时边界切换控制示意

2 ZC切换过程建模

2.1 基于MSC的系统建模

消息顺序图(MSC)是一种简洁的图形化描述语言，用来直观描述并行系统中各部件之间信息交互过程[8]。本文中采用MSC建立ZC切换场景的MSC模型，结合ZC切换过程中可能导致系统出现故障的各种情况，为后续时间自动机模型的建立提供依据。

定义：MSC是一个五元组，并且有MSC=(IMft{≤i}i∈l)用来描述ZC切换场景中各个子系统之间的信息交互关系，其定义如下。

(1)I={ITrain，IZC1，IZC2}分别表示车载子系统，移交ZC子系统和接管ZC子系统。

(2)M={MTrain，MZC1，MZC2}分别表示与车载子系统、移交ZC子系统及接管ZC子系统相关的消息集，其中MTrain={MAextendreq， ConnectZC1， Conf， Login1， Version1， Conf1， Control， MixedMA， ConnectZC2， Con-f4， LoginZC2， Version， Conf5， Pass， Conf6， Reqcontrol，Cancel， ControlT， Ackcancel};MZC1={MAextendreq， YG， Conf2， Conf3， Connect2， Routereq， MA2， MixedMA， ConnectZC1， Conf， Login1， Version1， Conf1， Control， Cancel， Ackcancel};MZC2={Connect2， Conf2， YG， Conf3， Routereq， MA2， Conf4， ConnectZC2， LoginZC2， Version， Conf5， Pass， Conf6， Reqcontrol， ControlT}。

(3)≤inst=Ui∈I。

(4)≤io={(!m，？m) |m∈M}。

定义中的f和t是从消息集M映射到实数集I上的函数，如f(MAextendreq)=ITrain，t(MAexte-ndreq)=IZC1。发送消息事件m用!m表示，接收消息事件m用？m表示，如：消息事件MAextendreq从Train子系统发送至ZC1子系统表示为，ZC1子系统接受从Train子系统发来的MAextendreq消息表示为。≤i表示实体i发生的事件对应到时间轴上的先后顺序，如对于实体Train上发生的两个事件MAextendreq和MixedMA，事件MAextendreq先于事件MixedMA发生。 ≤io表示对于任意一个消息事件，事件的发送先于接收发生，即∀m，!m≤io？m；如对于消息事件MAextendreq，Train子系统发送MAextendreq消息事件先于ZC1子系统接收MAextendreq消息事件发生。

根据以上定义，对ZC边界切换过程进行建模，假定切换过程中发生的消息事件都按正常的消息流程进行，根据消息事件发送、接收的因果关系，建立ZC切换过程的MSC模型，如图5所示。

图5 ZC边界切换过程MSC模型

2.2 模型描述

ZC切换过程中涉及的信息交互的对象有车载子系统(Train)，移交区域控制子系统(ZC1)，接管区域控制子系统(ZC2)。

(1)接近边界点(授权的终点为分界点)：列车在ZC1区域运行过程中，若某时刻Train收到了以边界点P为终点的移动授权，Train向ZC1发送授权延伸申请消息MAextendreq，然后ZC1向ZC2发送与ZC2建立通信连接的请求消息Connect2，ZC2向ZC1发送连接确认消息Conf2，相邻ZC间建立通信过程完成。ZC1向ZC2发送切换预告信息YG，并为列车申请ZC2范围内的进路，当联锁系统排出进路以后，ZC2将进路信息MA2发给ZC1，由ZC1将ZC1范围内进路信息与之混合后将新的授权信息MixedMA发送给列车，控制列车运行，如果在T5(5s)内Train没有收到MixedMA信息，则出现车地通信故障，实施紧急制动。

(2)车头越过边界点P：当列车车头越过边界点P后，Train收到切换执行应答器组(LTO)发送的执行转换消息，Train根据之前MixedMA中ZC2的信息，向ZC2发送与ZC2建立通信连接的请求消息ConnectZC2，ZC2向Train发送连接确认消息Conf4，连接ZC2成功后，Train向ZC2发送登录申请消息LoginZC2，ZC2将本身系统的版本号信息发送给Train，若版本号信息相同则Train向ZC2发送登录确认消息Conf5，否则Train系统从数据库存储单元(DSU)重新下载。

(3)车尾通过边界点P：当列车车尾越过边界点P后，Train向ZC2发送受控申请消息Reqcontrol，并向ZC1发送注销消息Cancel，当列车收到ZC2的控制消息ControlT后，ZC1向Train发送注销确认消息ACKcancel，整个切换过程结束，此后Train子系统在ZC2的控制下继续正常运行。

3 系统模型仿真

3.1 验证工具UPPAAL

时间自动机是在自动机理论基础上扩展的基于时间周期、时间约束和时间解释的实时系统建模方法[9]，相较于CPN、SPN及CSP，其主要优势在于有验证工具为其提供建模、仿真和验证环境[10]。UPPAAL通过模拟有限个控制结构和数值时钟来验证系统的安全性和受限活性[11-13]。

UPPAAL用户界面的编辑器、模拟器和验证器分别用于实时系统的建模、仿真和验证。模拟器不仅可以按状态转移检查状态的转移是否是期望的结果，当系统出现锁死时，还可以检查到出现锁死的部位继而对模型进行修正。验证器通过对状态空间的搜索来验证系统的功能属性和受限活性。UPPAAL专门为模型的验证提供了一种BNF语法[14-15]。具体语法含义如表1所示。

表1 BNF语法的含义

3.2 ZC切换过程模型

对于ZC切换过程的MSC模型仅仅直观描述了时间的进程，却无法对模型进行有效的分析和验证，所以需要将MSC模型描述的ZC切换过程转换成时间自动机模型，然后用UPPAAL工具对其进行验证。文中对ZC切换过程中涉及信息交互的3个活动对象分别建立各自的子时间自动机模型，即TATrain、TAZC1、TAZC2。ZC切换过程是这3个自时间自动机的积，即TA=TATrain||TAZC1||TAZC2。

图6为ZC切换过程的时间自动机网络模型。其中，以“!”为结尾的消息表示该条消息发出以后子系统位置发生转换，以“？”为结尾的消息表示收到该条消息后子系统位置发生转换，以此保证各子系统模型之间同一转换的同步发生。x、y、z和t为时钟约束，用于判断ZC1与ZC2的连接时间、Train与ZC2的连接时间、Train登录ZC2的时间以及ZC1计算MixedMA的时间是否超时。 routeorder、same和co mmunication为标志位，用于统一不同子系统间状态迁移的同步性。

图6 ZC边界切换时间自动机模型

4 模型验证

在UPPAAL用户界面的编辑器中建立ZC切换过程中各子系统对应的时间自动机网络模型并设置通道，在模拟器中对切换过程中出现的ZC1连接ZC2、ZC1申请进路、ZC2发送MA2、Train连接ZC2、Train登录ZC2、Train注销ZC1以及Train受控等信息的交互进行模拟校验。最后在UPPAAL中，利用BNF语法对ZC切换过程的性能和功能要求进行验证，验证结果如图7所示。

图7 模型验证结果示意

4.1 系统功能性要求

(1)系统无死锁现象：A []not deadlock，验证通过。

(2)在设备均正常的情况下，能实现列车控制权由ZC1向ZC2的切换：E <> (Train. Idle imply Train. Controled)，验证通过。

(3) 当列车越过ZC切换边界时，车载子系统能实现登录ZC2、数据库版本号校核以及与ZC1注销的功能：E <> ((Train. BuildLoginZC2) or (Train. Compaison) or (Train. Loginoff))，验证通过。

4.2 系统受限活性要求

(1)ZC1计算MixedMA信息的时间不超过T5：A <> ((ZC1. Routecheck imply ZC1. SendMixed MA) and (t

(2)若ZC1未收到ZC2发送的MA2信息，则无法计算出跨越切换边界的MA信息：A <> (not ZC1. CalculatenewMA) imply ZC1. SendMixedMA，验证不满足。因为ZC2范围内的进路是经ZC2计算后发送给ZC的，若无MA2，ZC1无法得出MixedMA。

(3)ZC1与ZC2连接时间不超过T2：A <> ((ZC2. Buildconn1 imply ZC2. Conn1YES) and (x

(4)车载子系统与ZC2连接时间不超过T3：A <> ((ZC2. BuildconnT imply ZC2. ConnTYES) and (y

(5)车载系统登录ZC2的时间不超过T4：A <> ((ZC2. Login imply ZC2. LoginYES) and (z

(6)当车载子系统在T5时间内没有收到跨越边界点的MA时，则认为车地通信系统出现故障，车载子系统进入紧急制动状态：A <> (Train. Approach and co mmunication==0) imply Train. Emerbreak，验证通过。

5 结论

基于通信的列车运行控制系统(CBTC)是一个结构比较复杂的实时系统，从ZC子系统的实际出发，将MSC半形式化方法作为描述ZC切换场景的切入点，然后使用时间自动机形式化方法对该切换过程进行描述和验证。首先，建立整个ZC边界切换场景中各子系统信息交互的MSC模型，其次，根据MSC模型的描述，建立时间自动机网络模型，最后，采用验证工具UPPAAL对ZC边界切换过程的功能属性和受限活性进行验证。结果表明：ZC边界切换功能满足设计要求，在通过地面分界点P时，列车控制权可以由移交ZC切换至接管ZC。因此，MSC与UPPAAL相结合的建模验证方法是可行的。

[1] 唐涛，郜春海，黄友能，等.CJ/T407—2012 城市轨道交通基于通信的列车自动控制系统技术要求[S].北京：中国标准出版社，2012.

[2] 王露，王长林.区域控制器移动授权的统一建模语言(UML)建模与验证[J].城市轨道交通研究，2014(7)：40-43.

[3] 李耀，陈荣武，郭进，等.基于TSSM的城市轨道交通CBTC区域控制器建模与验证[J].西南交通大学学报，2015(2)：27-34.

[4] 车玉龙，苏宏升.基于蒙特卡罗的CTCS-3级列控系统单元重要度分析[J].铁道标准设计，2013(8)：125-128.

[5] 刘金涛，唐涛，赵林，等.基于微分动态逻辑的无线闭塞中心交接协议建模与验证[J].中国铁道科学，2013(9)：98-103.

[6] 张友兵，唐涛.基于有色Petri网CTCS-3级列控系统RBC切换的建模与形式化分析[J].铁道学报，2012(7)：49-53.

[7] 黄友能，张鹏基，侯晓鹏，等.基于混成自动机的城市轨道交通ZC子系统建模与验证方法[J].中国铁道科学，2016(3)：114-120.

[8] Alur R， Etessami K， Yannakakis M. Inference of Message Sequence Charts[J]. IEEE Transaction on Software Engineering，2003，29(7)：623-633.

[9] 周翔，武晓春.基于MSC与UPPAAL的高铁跨界临时限速建模与验证[J].铁道标准设计，2016，60(10)：126-131.

[10] 曹源，唐涛，徐田华，等.形式化方法在列车运行控制系统中的应用[J].交通运输工程学报，2010(2)：122-123.

[11] 曹源.高速铁路列车运行控制系统的形式化建模与验证方法研究[D].北京：北京交通大学，2011.

[12] 万勇兵，徐中伟，梅萌.CTCS-3级列控系统临时限速服务器建模与形式化验证[J].系统仿真学报，2013，25(1)：132-138.

[13] Larsen K G， Mikucionis M， Nielsen B. Online Testing of Real-time System Using UPPAAL[C]∥International Conference on Formal Approaches to Software Testing， 2004，3395：79-94.

[14] 吕继东，唐涛，燕飞，等.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证[J].铁道学报，2009，32(3)：59-64.

[15] 康仁伟.基于时间自动机的CTCS-3级列控系统建模方法与研究[D].北京：北京交通大学，2013：40-53.