基于Timed RAISE的高速列车RBC切换协议形式化建模及验证

徐世泽，肖　蒙

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

基于Timed RAISE的高速列车RBC切换协议形式化建模及验证

徐世泽，肖蒙

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

摘要：在CTCS-3(Chinese Train Control System Level 3)级列控系统中，RBC(Radio Block Center)切换是影响列车安全高效运行的重要环节，现阶段对RBC切换协议进行验证分析所使用的形式化方法还存在状态爆炸或描述性质单一等问题。基于Timed RAISE的形式化方法，结合域的模型，在对RBC切换流程分析的基础上，构建状态转移图，得到切换协议的形式化模型，使用等价和推断的推理规则对模型的正确性和实时性进行推理验证，得到的结果表明，RBC切换协议满足规范标准对正确性与实时性的要求，将验证结果与其他文献的结论进行比较分析，说明该方法具有通用性，对于推广其在列控系统场景验证中的应用有一定的实际意义。

关键词：列控系统；形式化方法；RBC切换协议；正确性与实时性

引言

中国列车控制系统(Chinese Train Control System， CTCS)是我国铁路当中控制列车安全运行，提高列车行车效率的重要装备。无线闭塞中心(Radio Block Center， RBC)作为CTCS-3级列控系统的重要组成部分，其安全性、可靠性直接影响列车的安全运行。列控系统是一种复杂的安全苛求系统，无论是在标准和规范的制定过程当中，或是在系统的开发和设计阶段，都不可避免地会存在着一些系统的漏洞或安全隐患，在欧洲铁路行业规范标准IEC61508-1中明确指出，对于高安全部件(安全完善度等级SIL4级)，强烈推荐使用形式化方法进行建模和验证[1]。因此，使用形式化方法对RBC切换协议进行建模与验证是十分必要的。

文献[2]采用时间自动机理论对RBC的子系统进行了形式化的描述，建立了相应的网络模型，运用UPPAAL验证工具有效地证明了RBC子系统的安全性和受限活性，并对RBC切换的时间进行了优化。文献[3]结合UML和微分动态逻辑从列车混成性的角度对ETCS-2中的RBC交接场景进行建模，最后验证了其正确性并且得到了列车运行状况和RBC离散控制时间共同影响RBC交接效率的结论。文献[4]提出了一种基于列车主体性的RBC切换模型，由列车作为主体计算生成移动授权，同时运用Petri网对模型进行了形式化建模与验证，最后结论表明，新的模型增强了列车运行的安全性，提高了行车效率。文献[5]使用UML结合可达集计算的形式化方法，对CTCS-3级列控系统的RBC交接场景进行了建模和功能安全分析，分析的结果表明了UML与可达集计算相结合的方法适用于CTCS-3级列控系统的功能安全分析。上述文献对于列控系统中形式化方法的应用研究起到了积极的推动作用，但是仍存在以下的问题：(1)现阶段所使用的形式化验证方法较大部分都基于模型检验，当系统结构较为复杂，多任务并发运行时，系统状态空间会出现指数级增长，导致状态爆炸的问题；(2)列控系统由于其复杂的结构，包含了实时性、并发性、混成性和反应性等多种特性，目前所使用的基于定理证明的形式化方法都只针对了列控系统中的某一种特性，很难全面地描述和验证系统的全部特性。 在列控系统的结构愈加复杂的情况下，对单一性质的验证已不再适用，对高速铁路列控系统全面有效的验证更能提高效率[6]。本文采用了Timed RAISE的形式化方法，对CTCS-3级列控系统规范中的RBC切换协议进行建模，对系统模型的正确性和实时性进行验证，将验证分析的结果与其他文献的结论相比较，说明该方法的有效性。

1Timed RAISE形式化方法

Timed RAISE形式化方法包括了其规范语言RSL(RAISE Specification Language)和相应的开发工具集。在RSL中有3个主要的要素：type、value和axiom。type定义了所有数据的类型，value定义了函数以及常量的值，axiom定义了value的属性或者约束的规则，一般在axiom中，对所要验证的特性进行描述[7，8]。通过对以上3个部分灵活的运用和构建，可以实现模块化的建模方式以及对系统进程化的描述，实现了对列控系统混成性、并发性和反应性的支持。在RSL的不断研究过程中，又加入了时间因子Time，对系统的实时性能够很好地描述。Timed RAISE是基于定理证明的方法，使用数学逻辑来表示被验证的系统和所要验证的特性，可以用数学符号来描述具有无限状态空间的系统[9]。因此，使用Timed RAISE形式化方法能够更加全面深入的对列控系统进行建模和验证。

使用RSL标准语言进行建模与验证的框架图如图1所示。

图1　建模与验证框架

首先，对系统需求规范进行抽象，得到系统的域模型，使用RSL语言对系统域模型进行描述，得到了由逻辑表达式、命题、定理等构成的形式化模型。其次，使用RSL语言描述所要验证的系统性质，将其表示为公理、定理的形式。最后在验证时，使用推理规则对命题、定理等进行推理演绎，直至推导出最后的结果，判断其是否满足性质的要求。

2RBC切换过程

列车在运行过程当中从当前所处的RBC控制区域(移交RBC或RBC1)进入了下一个RBC控制区域(接受RBC或RBC2)，列车的控制权限要进行交接，这个过程就是RBC切换。RBC切换的过程可以分为双电台工作的情况和单电台工作的情况，采用双电台工作时RBC切换的过程作为研究的重点，切换步骤如下[10]。

(1)列车通过切换预告应答器组后，车载向RBC1发送列车位置报告，RBC1接到报告后向车载发送切换命令，同时向RBC2发送移交列车预告信息和进路请求信息。

(2)当RBC2接到进路请求信息后，向RBC1发送进路信息，RBC1根据得到的信息向车载发送延伸至RBC2区域的行车许可。

(3)车载根据RBC1提供的电话号码，使用电台2呼叫RBC2，呼叫成功则建立会话。

(4)当列车最大安全前端越过边界后，车载向RBC1和RBC2发送位置报告。之后，车载拒绝接受RBC1除终止会话信息之外的信息。同时，RBC2收到列车位置报告后向RBC1发送接管列车信息。

(5)当列车最小安全末端越过边界后，车载向RBC1和RBC2发送位置报告。RBC1接到位置报告后向车载发送切断通信命令，车载接到切断通信命令后，切断与RBC1的通信连接。

(6)车载通过电台2与RBC2保持通信会话并接受行车许可，监控列车安全运行，完成了RBC1到RBC2的切换。

3RBC切换协议的建模与验证

3.1域模型的建立

为了降低建模的难度，方便RSL语言进行描述，首先建立系统的域模型。域是一类有着相同的性质和功能的模型合集，可以将整个RBC切换的流程看作一个域，域模型的基本结构如图2所示。在域模型中，包括了3个基本的要素，输入、输出和函数，图2中IN表示域的输入，包括了列车和RBC的状态，参数等，F(I)表示域函数，其中I表示域的输入，即IN，O表示输出，即OUT，这些输入在域函数F的作用下，不断发生改变，直至域的输出OUT。列车和RBC之间不断地进行信息交互使得状态发生变化，函数F表示了列车和RBC的状态不断迁移变化的过程。列车运行以及RBC正常工作的过程都是在时间上连续的，以列车与RBC通信时信息的传递为分界，可以将整个连续的过程转化为在时间上离散的过程，得到RBC切换协议的状态转移图，如图3所示。

图3中RBC1为移交RBC，RBC2为接收RBC，竖线是时间的顺序，方框中内容是执行的事件，图中清晰地描述了2个相邻的RBC在移交列车时，系统状态的迁移变化过程。

图2　域模型结构

图3　状态转移

3.2RSL模型的建立

根据图3中RBC切换场景的状态转移过程以及需求标准对网络传输的延时要求[11]，建立RBC切换协议的RSL模型。为了方便建模，对图3中的每一个状态进行了编号，R11表示RBC1的第一个状态，T1表示列车的第一个状态，R21表示RBC2的第一个状态，其他与之类似。RSL模型由列车子模型Train、RBC1子模型、RBC2子模型和网络传输子模型Delay组成，模型的描述具体如下。

1) 列车子模型

根据切换协议以及状态转移图，建立列车的RSL模型Train，在Train模型中描述了列车发送位置报告，与RBC2建立通信等工作过程，具体的模型如下。

class

type

Train，

Train_state==T1| T2| T3| T4| T5| Tok| Terror

value

t：Train， r1，r2：RBC， g1，g2：NET

Train_def： Train×NET×NET→Train×NET×NET

Train_def(t，g1，g2)≡case state(t) of

T1→T1_work(t，g1)， T2→T2_work(t，g1，g2)

Tok→ (t，g1，g2)， Terror→ (t，g1，g2)

end

//T1state//

T1_work: Train×NET →Train×NET

T1_work(t，g1)≡Train_send(Loc_mes(t，r1)，g1);

change_state(T2)

//T2state//

T2_work: Train×NET ×NET→Train×NET×NET

T2_work(t，g1，g2)≡

let (mes，g1)=Train_get(g1) in case mes of

RBC_com(r1，t)→Train_send(RBC_call(t，r2)，g2);

change_state(T3)

nil→(t，g1，g2)， error→change_state(Terror)

end end

Train的模型中，Train_state表示列车的状态，Tok是列车完成切换后的成功状态，Terror是错误的状态。t，r1，r2，g1，g2分别表示列车，RBC1，RBC2和两个车载电台。Train_def表示列车在不同状态时要执行的动作。在状态T1中，Train_send表示列车发送位置报告Loc_mes，change_state表示列车的状态迁移进入了状态T2。在状态T2中，列车根据收到的消息Train_get判断下一步的动作，若收到切换命令RBC_com，那么列车向RBC2发送呼叫消息RBC_call，若收到空消息nil则不动作，若收到错误消息error则进入错误状态Terror。列车其他状态的模型与T1，T2相似，只是发送接受的消息不同，以T1，T2为例进行说明，其他不再表述。

(2)RBC子模型

根据切换协议和状态转移图，建立RBC的RSL模型，因为RBC1和RBC2是同一类型设备，将两者放在同一模块中建模。RBC模型描述了RBC发送切换命令、进路请求信息和行车许可等工作过程，具体模型如下。

class

type

RBC，

RBC1_state==R11| R12| R13| R14|

R15| R1ok| R1error

RBC2_state==R21| R22| R23| R24|

R25| R2ok| R2error

value

t: Train， r1，r2: RBC， g1，g2: NET

RBC1_def:RBC×NET →RBC×NET

RBC2_def:RBC×NET →RBC×NET

RBC1_def(r1，g1)≡case state(r1) of

R11→R11_work(r1，g1)， R1ok→ (r1，g1)，

R1error→ (r1，g1)

end

RBC2_def(r2，g2)≡case state(r2) of

R21→R21_work(r2，g2)， R2Fok→ (r2， g2)，

R2error→ (r2，g2)

end

//R11state//

R11_work: RBC×NET →RBC×NET

R11_work(r1，g1) ≡

let (mes，g1)=RBC1_get(g1) in case mes of

Loc_mes(t，r1) →RBC1_send(RBC_com(r1，t)) ||

RBC1_send_RBC2(Route_req(r1，r2));

change_state(R12)

nil→(r1，g1)， error→change_state(R1error)

end end

RBC的模型中，RBC1_state和RBC2_state分别表示两个RBC的状态，状态的定义和设备的定义与列车子模型中的相同，在状态R11中，RBC1若收到列车的位置报告Loc_mes，则向列车发送切换命令RBC_com，同时向RBC2发送进路请求信息Route_req，若收到空消息则不动作，若收到错误消息error则进入错误状态R1error，正确执行动作后进入状态R12。RBC1与RBC2的其他状态模型与R11相似，以R11为例进行说明，其他不再表述。

(3)网络传输子模型

根据文献[11]中对网络传输时延的要求，建立网络传输的RSL模型Delay。为了方便建模，将越区切换、链路中断、突发降质等因素造成的通信故障都简化为信息传输的延时，具体的模型如下。

type

Time，

Mes_delay={t：Time · 0.5

Build_delay={t：Time · 5

Reg_delay={t：Time · 15

TTI_delay={t：Time · 0

在Delay模型中，Mes_delay表示端到端信息传输的延时时间，Build_delay表示连接建立的网络延时，Reg_delay表示网络注册的延时时间，TTI_delay表示传输干扰带来的网络延时，时间都是以s为单位。

3.3RBC切换协议的验证

为了保证列车运行的安全与效率，对RBC切换协议的要求是：在一定的时间内，列车能够安全可靠地完成RBC切换，并且不影响列车的行车效率。因此，对RBC切换协议的正确性和实时性进行了验证。

(1)正确性验证

由域模型的分析可以得到，在图3的状态转移图中，T1，R11和R21三个初始状态就是域模型的输入，而T5，R15和R25三个最终状态是域模型的输出。列车安全可靠完成RBC切换的充分必要条件是：从域模型的输入开始，经过状态的变迁，最终列车，RBC1和RBC2到达了域模型的输出，即T5，R15和R25三个最终状态，若在过程中，发生了系统死锁，信息交互错误，系统都会进入错误状态，无法完成RBC切换。根据切换正确性的分析，运用RSL语言对所验证性质进行描述，使用推理规则对正确性进行验证，具体描述如下。

axiom

[Handover_correct]

∀ t∶Train， r1，r2∶RBC， g1，g2∶NET ·

Train_state(t)=T1 ∧ RBC1_state(r1)=R11 ∧

RBC2_state(r2)=R21 ∧ Train_get(t，g1，g2)=nil ∧

RBC1_get(r1，g1)=nil ∧ RBC2_get(r2，g2)=nil

⟹ let (t’，r1’，r2’，g1’，g2’)=erg(t，r1，r2，g1，g2) in

Train_state(t’)=Tok ∧ RBC1_state(r1’)=R1ok ∧

RBC2_state(r2’)=R2ok

end

在正确性的RSL描述[Handover_correct]中，erg表示对整个系统状态进行遍历，Train_state(t’)=Tok ∧ RBC1_state(r1’)=R1ok ∧ RBC2_state(r2’)=R2ok表示列车，RBC1和RBC2最终进入了正确的状态，同时也是最终要验证的目标。

使用推理规则中的等价规则(equivalence rules)和推断规则(inference rules)，结合列车子模型和RBC子模型，对正确性的RSL描述进行推理演绎，经过整理最终得到了下面的表达式。

Train_state(t’)=Tok∧RBC1_state(r1’)=R1ok∧

(1)

式(1)表明列车，RBC1和RBC2经过状态迁移最终进入了正确的状态，即列车能够安全可靠的完成RBC的切换。结果说明了RBC切换协议满足系统对于切换正确性的要求。

(2)实时性验证

文献[11]中规定，列车注册下一RBC分区的时间必须在 40s内完成。假设列车以300km/h的速度运行，且列车长度为400m，则从列车前端通过切换点，到列车末端通过切换点共需要4.8s时间，则总共RBC切换的时间为44.8s，当RBC切换时间大于44.8s，则会影响列车的行车效率。运用RSL语言对RBC切换的实时性要求进行描述，使用推理规则对实时性进行验证，具体描述如下。

axiom

[Handover_time]

Time_totle=Time_pass(T1)+Time_pass(R11)+

Time_pass(T2)+Time_pass(R22)+Time_pass(T4)

⟹Time_totle≤ 44.8

其中，Time_pass表示在状态内的信息交互，网络注册等所需要的时间，Time_totle≤ 44.8是最终要验证的目标。

与验证RBC切换正确性的过程相同，使用推理规则，结合列车子模型和RBC子模型对实时性的RSL描述进行推理演绎，最终得到下面的表达式。

(2)

式(2)表明，在正常的网络状况下，RBC切换的时间小于44.8 s，即列车能够在要求的时间内完成切换，说明了RBC切换协议满足系统对于实时性的要求。

(3)文献比较分析

对于RBC切换正确性的验证，文献[12，13]分别采用了通信顺序进程和Petri网两种形式化方法对RBC切换过程进行了验证，采用的切换协议与本文相同，最后验证的结果都表明切换协议的正确性满足系统的要求，这与本文的研究结果一致。

在不同网络质量的情况下，对RBC切换过程的实时性进行验证，验证的结果与文献[14]相比较，如表1所示。

表1　验证结果比较

表1中，“实时性验证”是本文得到的验证结果，结果显示，在网络质量为60%、70%和80%时，切换过程不满足实时性的要求，由于RSL模型是由数学逻辑表达式构成的，所以得到的结果为布尔值。“切换时间”是文献[14]中，经过仿真运行得到的RBC切换时间的数据，在网络质量为60%、70%和80%时，切换的时间分别为55.1、52.8 s和45.8 s，都大于44.8 s，不符合实时性的要求，这与本文研究结果一致。当网络质量为90%和100%时，两者的验证结果同样相同。

通过以上的比较分析，证明了Timed RAISE方法能够全面有效地对系统协议进行建模与验证，说明了该方法适合于CTCS-3级列控系统场景的形式化建模与验证分析。

4结论

在现阶段针对铁路列控系统进行形式化验证的方法中，还存在着状态爆炸和描述性质单一等问题，这大大制约了形式化方法的应用范围，基于定理证明的Timed RAISE方法不会产生状态爆炸的问题，同时能够更加全面的验证整个系统。本文首先分析了RBC切换协议的整个过程，为了降低建模难度，使用了域的方法对切换协议进行了抽象建模，得到了相应的域模型，然后使用RSL标准语言对域模型进行描述，建立了切换协议的形式化模型，最后对切换协议的正确性和实时性进行了形式化描述，并使用相关的推理规则进行推理演绎，得到了验证的结果，结果表明RBC切换协议满足相关的安全性和实时性的要求。将验证结果与其他文献的结论进行比较分析，说明了该方法的有效性，对于推广其在列控领域场景验证中的应用有一定的实际意义。

参考文献：

[1]BOWEN J P. Formal Methods in Safety-Critical Standards[C]∥Software Engineering Standards Symposium. Brighton: IEEE Computer Society Press， 1993:168-177.

[2]吕继东，唐涛，贾昊.客运专线CTCS-3级列控系统无线闭塞中心的建模与验证[J].铁道学报，2010，32(6):34-42.

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

[4]潘登，梅萌，郑应平.基于列车主体性的RBC越区切换模型[J].交通运输系统工程与信息，2013，13(4):134-141.

[5]刘金涛，唐涛，赵林，等.基于UML模型的CTCS-3级列控系统功能安全分析方法[J].铁道学报，2013，35(10):59-66.

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

[7]顾翔，邱建林，邵浩然.基于RSL的协议形式化描述与验证方法[J].计算机工程，2009，35(23):41-43.

[8]Xiang Gu， Jianlin Qiu. Describing Protocol Elements and Protocols with RSL[C]//Advances in Information Technology and Industry Applications. Berlin: Springer， 2012：741-748.

[9]章珍珍.高速磁浮运控系统运行场景的RSL建模与验证[D].北京:北京交通大学，2013.

[10]李伟.基于有色Petri网的无线闭塞中心子系统切换建模与验证[D].北京:北京交通大学，2009.

[11]铁道部.科技运[2008]168号CTCS-3级列控系统GSM-R网络需求规范(v1.0)[S].北京:中国铁道出版社，2008.

[12]吕继东，唐涛.高速铁路列控系统运营场景实时性的建模与验证[J].铁道学报，2011，33(6):54-61.

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

[14]杨柳倩.基于UML和有色Petri网的RBC切换建模与分析[D].兰州:兰州交通大学，2012.

The Formal Modeling and Verification of RBC HandoverProtocol for High-speed Train Based on Timed RAISE

XU Shi-ze， XIAO Meng

(School of Automation and Electrical Engineering， Lanzhou Jiaotong University， Lanzhou 730070， China)

Abstract：In the CTCS-3-based train control system， the Radio Block Center (RBC) handover is an important part closely related to train safety and efficiency. The formal methods used for verifying and analyzing train control system tend to have some problems such as state explosion and singularity of description. Based on the analysis of RBC handover， the Domain method merging with Timed RAISE formal is applied to construct state transition diagram and obtain the formal model of handover protocol， and the inference rules are used to verify the correctness and real time of handover protocol. The result shows that the protocol satisfies the requirements for correctness and real time. The verification results are compared with other literatures and proved to be suitable for scene verification in train control system.

Key words：Train control system; Formal method; RBC handover protocol; Correctness and real time

中图分类号：TP301.2

文献标识码：A

DOI:10.13238/j.issn.1004-2954.2015.06.031

文章编号：1004-2954(2015)06-0138-05

作者简介：徐世泽(1989—)，男，硕士研究生，E-mail：348510010@qq.com。

收稿日期：2014-12-15； 修回日期：2014-01-12