基于MSC与UPPAAL的高铁跨界临时限速建模与验证
2016-10-15武晓春
周 翔，武晓春
(兰州交通大学自动化与电气工程学院，兰州 730070)
基于MSC与UPPAAL的高铁跨界临时限速建模与验证
周翔，武晓春
(兰州交通大学自动化与电气工程学院，兰州730070)
临时限速服务器是高铁列控系统的重要组成部分，其不仅要校验CTC下发的临时限速命令，还要与相邻调度台临时限速服务器之间进行频繁的信息交互，因此对其安全性和实时性要求也更苛刻。为了满足高铁列控系统对其运行的要求，采用时间自动机理论和消息顺序图(MSC)相结合的方法，首先建立跨界临时限速命令的MSC模型和时间自动机子模型，再利用UPPAAL验证工具对形式化语法BNF描述的时间自动机子模型属性进行验证。根据仿真验证结果确认了跨界临时限速信息的安全性和受限活性，为进一步开发临时限速服务器功能提供了重要的依据。
临时限速服务器；时间自动机；UPPAAL；实时性；MSC
随着我国高速铁路的快速发展，高铁列控系统对临时限速服务器的安全性和实时性的要求也越来越高。临时限速服务器是高铁列控系统的重要组成部分，其工作流程具有严格的时间约束特性和安全特性，是典型的实时系统[1-2]。因此，根据高速列车的实际运行情况，临时限速区段可能设置在CTCS(Chinese Train Control System)等级转换区，此时，等级转化区一侧为客运专线CTCS-2/CTCS-3级控制区域，另一侧为既有提速线控制区域[3-4]。由于其设备之间信息交互的复杂性，利用半形式化(以数学为基础来定义硬件系统和软件系统的规约但不对其进行验证)和形式化方法对跨界临时限速区域临时限速命令的拟定下达校验进行建模和验证，有效地发现系统硬件设计和时间约束缺陷，提高其系统的安全性和受限活性。
半形式化方法以MSC(Message Seque-nce Chart)消息顺序图为基础，描述临时限速命令的交互过程；形式化方法以离散型数学为基础，运用严格的形式化语义对系统特性进行精确描述，其中时间自动机是形式化方法中一种，不仅可用来描述实数值时钟约束系统，还可以描述有限控制变量的状态转换系统[5]。因此，利用MSC对CTCS等级转换区跨界临时限速与各相关设备信息交互流程建立模型将其转化为时间自动机模型，并利用UPPAAl验证跨界临时限速的安全性和受限活性。
1 CTCS等级转换区临时限速场景分析
在高铁列控系统中，临时限速服务器不仅对临时限速命令进行校验和存储，而且还要跟其他相关信号设备进行交互。如：CTC(Centralized Traffic Control，调度中心)负责拟定、执行、取消等命令的下达，TSRS(Temporary Speed Restriction Server，临时限速服务器)完成校验、分发和综合，并将结果反馈给CTC，TCC(Train Control Center，列控中心)、RBC(Radio Block Center，无线闭塞中心)分别通过应答器、GSM-R(Global System for Mobile Communication-Railway)将TSRS下发的TSR(Temporary Speed Restriction，临时限速命令)发送到车载设备执行[6-7]。临时限速在CTCS等级转换区的场景如图1所示。
图1 CTCS等级转换区临时限速场景
临时限速命令的拟定遵循“以线路正方向为限速起点”的归属原则，限速-2在两侧TSRS数据覆盖范围之内。因此，TSRS-A与TCC-B要实现TSR切换控制权同步，这样临时限速命令正式生成。本论文主要是针对CTCS等级转换区的跨界临时限速命令的拟定下达、取消和删除过程进行建模[8]，从而验证跨界临时限速命令切换的安全性和时效性。
2 MSC模型描述
2.1基于MSC的系统建模
消息顺序图(MSC)是一种直观可视的半形式化图形描述语言，用来描述不同组件之间交互机制。MSC的描述功能能够满足许多复杂领域的应用，因此，利用MSC来描述等级转换区跨界临时限速TSR切换的过程，建立技术规范中模型的信息交互和状态转移(静态)过程，为后面的模型搭建提供清楚的图形描述，从而达到验证的目的。
定义1：MSC是一个五元组∑=(I，M，f，t，{≤i}i∈I)。其中，I是有限实体集，M是有限消息集，f∈M→I、t∈M→I分别表示消息接收和消息发送，对∀i∈I，≤i={？m∣m∈M，t(m)=i}∪{!m∣m∈M，f(m)=i}，即M中消息接收与消息发送的传递闭包。
定义2：假定一个五元组MSC=(I，M，f，t，{≤i}i∈I)可以用来描述等级转换区跨界临时限速命令交互模型，其定义如下。
(1)I={ICTC-A，ITSRS-A，ITCC-B，ICTC-B}，分别表示仿真客专侧CTC系统，客专侧TSRS系统，既有线侧TCC系统，既有线侧CTC系统。
(2)M={MCTC-A，MTSRS-A，MTCC-B，MCTC-B}，分别表示仿真客专侧CTC系统，客专侧TSRS系统，既有线侧TCC系统，既有线侧CTC系统的相关消息子集。
(3)≤inst=Ui∈I。
(4)≤io={(!m，？m)∣m∈M}。
(5)≤MSC=(≤inst∪≤io)+。
其中：MCTC-A={SetTSR，ActivateTSR，DisToTCC，ActTSR}，MTSRS-A={SaveTSR，ActFail，CancTSR，NoticeCase，ActTSR，JudCommand，ExeTSR，DisToTCC-B，Protocal(TSRSToCTC)}，MTCC-B={ActSucc，NoticeCase，ExeTSR，ExeSucc}，MCTC-B={NoticeCase，SetTSR，Protocal(CTCToTSRS)}，f和t表示将消息集M映射到实数集I的函数，如f(SetTSR)=ICTC-A，t(SetTSR)=ITSRS-A。!m用来表示发送m事件，？m用来表示接收m事件，如：消息SetTSR从组件CTC-A发送至组件TSRS-A表示为
2.2跨界临时限速命令的拟定和下达
如图1中限速-2由CTC-A负责拟定a-c段，CTC/TDCS-B负责拟定c-b段。若左侧调度台CTC-A下发SetTSR消息至TSRS-A，由TSRS-A对下发命令进行校验，此时TSRS-A向CTC-A反馈校验结果需要在4个通信周期完成(一个通信周期为2s)，若CTC-A在2s内没有收到反馈校验结果则判断为一次等待超时，若CTC-A向TSRS-A重发消息且连续4次等待超时则判断CTC-A与TSRS-A之间通信中断。当校验成功时回执SaveTSR消息至CTC-A，其校验MSC模型流程如图2所示。CTC-A根据反馈回的SaveTSR，向激活后的TSRS-A发送ActTSR消息。TSRS-A根据命令参数信息将临时限速命令下发至TCC-A，同时发送至右侧区域TCC-B进行验证、执行。此时TSRS-A要求TCC-A，TCC-B要在3个通信周期(一个通信周期为1s)内反馈接受信息，如果没有接收到反馈信息则判断一次等待超时，如果连续3次判断为等待超时则TSRS-A判断为通信中断。同时要求TCC-A、TCC-B将验证、执行的有效的目标参数结果反馈给TSRS-A。TSRS-A对目标验证结果进行综合判定，若验证成功向CTC-A发送ActSucc消息，若验证失败向CTC-A返回ActFail消息。当验证目标信息成功时，CTC-A向TSRS-A发送ExeTSR消息，由TCC-A和TCC-B执行临时限速命令，并将执行成功的ExeSucc消息反馈给TSRS-A。
图2 客专侧临时限速命令的校验MSC模型
若由右侧的CTC/TDCS-B下发的SetTSR消息发送至TCC-B，左侧TSRS-A通过CTC协议转换Protocal(CTCToTSRS)接收TCC-B下发的SetTSR消息由其进行可执行性校验(校验流程图如图3所示)，此时既有线侧同客专侧通信周期相同。
图3 既有线侧临时限速命令的校验MSC模型
若校验成功，发送ActSucc消息至本侧的TCC-A，并由TCC-B发送ExeTSR消息至CTC-A执行临时限速命令；若校验失败，TSRS-A将ActFail消息发送至右侧调度台CTC/TDCS-B，并将CancTSR消息发送至TCC-B。反馈两侧执行信息由TSRS-A综合校验，其结果发送至左侧调度台CTC-A显示。
2.3跨界临时限速命令的取消与删除
客运专线调度台CTC-A由原拟定方取消临时限速命令拟定的限速命令；而既有提速线调度台CTC/TDCS-B需要通过电话、传真通知客运专线调度台确认，只有得到确认后，才能由CTC/TDCS-B下达取消命令[11]。
3 系统建模仿真
3.1时间自动机与UPPAAL
时间自动机理论由R.Alur和Dill于1994年提出，时间自动机是一种基于时间周期、时间约束和时间解释的形式化建模方法。UPPAAL验证工具由Aalborg大学和Uppsala大学于1995年共同开发，其通过模拟控制有限个控制结构和数值时钟并采用整型变量来验证系统的安全性和受限活性[12-13]。
UPPAAL用户界面包括三个部分：系统编辑器(system editor)、模拟器(simulator)和验证器(verifier)。其中system editor用于创建和编辑要分析的系统；simulator用来检查所建系统模型是否正确；verifier通过快速搜索系统模型的状态空间来检查时钟约束条件和限制性质。UPPAAL验证工具应用的BNF语法[14-15]。Prop::=E<>p∣E[]p∣A<>p∣A[]p∣p→q，这种语法含义如表1所示。
表1 BNF语法及其含义
3.2基于时间自动机的跨界临时限速的模型
2.1节和2.2节已利用消息顺序图(MSC)对跨界临时限速命令在设备之间的交互流程已做了详细的阐述，且根据MSC描述的流程用UPPAAL建模仿真工具分别对CTCS等级转换区跨界临时限速信息交互的4个活动对象进行建模，即CTC-A、TSRS-A、TCC-B、CTC-B。构造出每个时间自动机模型，分别为TACTC-A、TATSRS-A、TATCC-B、TACTC-B，如图4所示。
设CTCS等级转换区跨界临时限速的时间自动机模型为
TA=
S、S0、A、X、I、E分别表示时间自动机建模的过程状态、初始状态、触发事件、时间参数、整数变量、状态转移路径。其中，过程状态S={idle，P_preTSR，S_exeFail，S_exeTSR，…};初始状态S0=idle;触发事件A={cancelTSR，TSRFail，warning，planTSR，…};时间参数X={T0，T1，T2，t，T_TCCreaction，T_TSRStimeout}，其中T0表示临时限速命令激活提示时间，T1、T2用来表示TSRS与TCC和CTC之间的通信时间，T_TCCreaction表示TCC接收和反馈TSRS发送信息的等待时间，T_TSRStimeout表示接收反馈信息超时;整数变量I={confirmFlag，verifFlag，checkFlag，exeFlag};状态转移路径E={idle，comfirmFlag，P_preTSR，confirmFlag，idle，…}。其中“P_”，“E_”，“S_”开头分别表示限速命令的拟定、下达、设置的过程。
如图4所示，跨界临时限速时间自动机网络模型。其中，“!”表示发出信息交互，“？”表示接受信息交互。标有C的圆圈为坚定位置，表示在没有时间延迟的情况下立即转换离开约束位置，在该位置进行操作具有原子性，使用它则可以明显减少系统状态空间，并且可以对多个同步通信进行编码。图中模型中的主要位置如表2所示。
表2 模型中的主要位置
图4 CTCS等级转换区跨界临时限速的时间自动机模型
4 系统模型的验证
图5 跨界临时限速工作状态流程时序
在UPPAAL模拟器中建立好CTCS等级转换区跨界临时限速的时间自动机网络模型，其工作流程时序如图5所示；同时在模拟器中对跨界临时限速命令的拟定下达、取消与删除等信息的交互进行模拟校验；最后在UPPAAL验证器中，应用BNF语法对跨界临时限速的时间自动机模型进行验证从而满足其安全性和受限活性的要求，如图6所示。
图6 性质验证
4.1系统安全性要求
(1)TSRS-A分发跨界临时限速命令进行校验，E<>(TSRS_a.idle)imply(TSRS_a.E_waitCheck);同时请求邻站TCC-B校验，E<>(TCC_b.idle)imply(TCC_b.S_check).验证通过。
(2)TSRS-A对执行跨界临时限速命令进行验证，E<>(TSRS_a.idle)imply(TSRS_a.S_verif);同时请求邻站TCC-B进行执行校验，E<>(TCC_b.S_checkSucc)imply(TCC_b.S_verif).验证通过。
(3)TCC-B应向TSRS-A反馈分发校验结果，E<>(TCC_b.S_check)imply(TCC_b.S_sendCheckRes);TSRS-A对结果进行校验，E<>(TSRS_a.E_waitCheck)imply(TSRS_a.S_checkRes)).验证通过。
(4)TCC-B应向TSRS-A反馈执行验证结果，E<>((TCC_b.S_verif)imply(TCC_b.S_sendVerifRes);TSRS-A对执行结果进行验证，E<>(TSRS_a.S_waitVerif)imply(TSRS_a.S_verifRes).验证通过。
(5)TCC-B既没有发送执行反馈信息，TSRS-A也没有向CTC-B报警。
E[]((not((TCC_b.S_exeTSR)imply(TCC_b.S_exeFinish)))and(not((CTC_b.S_exeTSR)imply(CTC_b.idle)))and(T2>T_TSRStimeout)).验证不通过，因为无反馈信息无报警这种情况是不允许发生的。
4.2系统受限活性要求
(1)TCC-B收到临时限速命令后，其验证结果要求在1s反馈回TSRS-A，由TSRS-A对TCC-B反馈的验证结果进行判定。
A<>(TCC_b.S_exeTSR)imply(TCC_b.S_exeFinish)and(T1<=1).验证通过。
(2)TSRS-A对限速信息进行有效性校验，并在2 s内向CTC-A行调台反馈校验结果。若校验成功，临时限速操作终端需每隔10 min向CTC-A提示临时限速命令的激活。
A<>((TSRS_a.P_checkValidity)imply(TSRS_a.P_checkSucc)or(TSRS_a.P_checkValidity)imply(TSRS_a.P_checkFail)and(T2<2)and(CTC_a.S_judgeCheckRes)imply(CTC_a.S_waitConfirm)and(T0=600).验证通过。
(3)TSRS-A在超出T_TSRStimeout时间未收到反馈信息，则报警。
A<>((TSRS_a.S_waitRes)imply(TSRS_a.idle)and(T2>T_TSRStimeout)).验证通过。
以上每条性质都逐一进行了验证，通过分析说明该系统满足实际中对CTCS等级转换区跨界临时限速安全性和受限活性的要求。
5 结语
本文采用消息顺序图(MSC)和时间自动机这种形式化的方法对跨界临时限速进行建模，应用MSC建立起整个跨界临时限速信息交互系统的模型，详细阐述模型中信息交互和状态转移过程，并根据MSC描述的此过程同时建立时间自动机网络模型，且应用UPPAAL进行模型验证。成功地验证了CTCS等级转换区跨界临时限速的安全性和受限活性，保证了系统的平稳运行，并为系统进一步开发提供重要的依据。
[1]吴永刚，陆慧娟.基于时间自动机的实时系统建模及验证[J].计算机时代，2011，6(1):2-3.
[2]郭震.CTCS各级系统中临时限速技术运用的探讨[J].科技信息，2011(16):111-112.
[3]姜明华.列控系统级间转换点临时限速区段设置探讨[J].铁道通信信号，2013(4):32-33.
[4]刘传会，张广全.一种基于时间自动机网络的实时系统形式化验证方法[J].苏州大学学报，2008，24(1):35-40.
[5]中华人民共和国铁道部.科技运[2010]137号.客运专线列控系统临时限速技术规范(V2.0)[S].北京：中华人民共和国铁道部，2010.
[6]甄力剑.客运专线临时限速技术研究与应用[D].成都:电子科技大学，2012.
[7]袁磊，王俊峰.CTCS-3级列控系统临时限速建模与验证[J].西南交通大学学报，2013，48(4):701-712.
[8]康仁伟.基于时间自动机的CTCS-3级列控系统建模方法与验证研究[D].北京:北京交通大学，2013：40-53.
[9]万勇兵，徐中伟，梅萌.CTCS-3级列控系统临时限速服务器建模与形式化验证[J].系统仿真学报，2013，25(1):132-138.
[10]胡雪莲，陶彩霞.基于MSC与UPPAAL的列控系统等级转换场景形式化验证[J].铁道标准设计，2015(2):122-127.
[11]赵荣亮，王长林.高速铁路CTC分界口临时限速系统建模与验证[J].铁路计算机应用，2014，23(7):43-47.
[12]Larsen K G，Mikucionis M，Nielsen B.Online Testing of Real-time System Using UPPAAL，Formal Approaches to Software Testing-4th International Workshop[J].Lecture Notes in Computer Science:(S0302-9743)，2005,3395:79-94.
[13]曹源.高速铁路列车运行控制系统的形式化建模与验证方法研究[D].北京:北京交通大学，2011.
[14]吕继东，唐涛，燕飞，等.基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证[J].铁道学报，2009，32(3):59-64.
[15]Hessel A，Larsen K G，Mikucionis M.Testing real-time systems using UPPAAL[J].Lecture Notes in Computer Science, 2008,4949:77-117.
Modeling and Verification of Cross-border Temporary Speed Restriction for High Speed Railway Based on MSC and UPPAAL
ZHOU Xiang，WU Xiao-chun
(College of Automation &Electrical Engineering，Lanzhou Jiaotong University，Lanzhou 730070，China)
Temporary Speed Restriction Server (TSRS) is an important part of the High Speed Railway Train Control System，it not only checks the temporary speed restriction orders issued by CTC，but also exchanges information frequently with the temporary speed restriction server of the adjacent dispatching station，and the requirements for its security and real-time performance are rigorous.In order to meet the requirement of the high speed railway train control system，a combination of timed automata theory with Message Sequence Chart (MSC) is employed to establish firstly the MSC model of Cross-border Temporary Speed Restriction and timed automata submodel，and then the verification tool of UPPAAL is used to verify the properties of the Cross-border Temporary Speed Restriction System described by BNF syntax.According to the simulation verification results，the security and restricted activity of the Cross-border Temporary Speed Restriction Information are confirmed，which provides an important basis for further development of the Temporary Speed Restriction Server.
Temporary Speed Restriction Server; Timed automata; UPPAAL; Real-time; MSC
2016-03-15；
2016-04-13
国家自然科学基金地区项目(61164010)
周翔(1989—)，男，硕士研究生，E-mail：826791444@qq.com。
1004-2954(2016)10-0126-06
U284.48+2
A
10.13238/j.issn.1004-2954.2016.10.028
