基于TRSL的RBC等级转换场景研究

陈永刚，丁春平

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



基于TRSL的RBC等级转换场景研究

陈永刚，丁春平

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

无线闭塞中心等级转换场景作为中国列车运行控制系统主要场景之一，切换成功与否直接影响高速列车的安全和运行效率。通过对形式化验证方法的分析，采用基于定理证明的时间化工业软件工程规范语言的严格方法(Timed Rigorous Approach to Industrial Software Engineering Specification Language，TRSL)，在对等级转换过程进行分析的基础上，设计交互信息图，构建状态迁移图，并结合域建模方法实现对该场景的TRSL描述，最后利用语言推理规则，结合系统特性，实现对切换正确性和实时性的双重验证，结果表明：该场景满足系统规范对功能性和实时性的要求，继而说明该方法的有效性、正确性和通用性，为我国列控系统的设计开发和验证提供一种新的途径和依据。

列车运行控制系统；RBC等级转换；TRSL；场景切换正确性

为保证高速列车安全、高效地运行，我国铁路部门在参照欧洲列车控制系统的基础上，研发了满足我国铁路线路的中国列车运行控制系统(Chinese Train Control System，CTCS)[1]。CTCS-3级列控系统具有分布式结构、连续式响应、实时性强的特性，如何选取有效而又合适的方法来实现系统特性的描述和验证，已成为高铁列控系统研究领域中的重要研究内容。目前，一般通过3种手段：仿真、测试以及最具严格性的形式化方法来验证系统特性，由于前两者的代价昂贵、花费时长，而且只能在系统投入前处理典型情况，无法实现状态、路径的穷举遍历[2]，针对安全苛求系统，采用形式化方法不仅可实现更严谨的系统描述和验证，而且可避免以上方法的不足[3，4]。

形式化方法可以精准地表述系统结构、行为、特征以及时间要求等，用形式化方法描述系统需求规范要求，可以最大程度地找出其他方法中忽视的错误和缺陷，同时还可以运用严格的数学逻辑实现对系统特性的验证分析，来判断系统特性是否成立[5]。

模型检验和定理证明是两种形式化验证方法，前者穷尽搜索系统状态，验证特性不满足时可给出反例实现错误定位，然而，当架构复杂的系统有多个并发任务时，会产生状态爆炸问题[6，7]；定理证明利用数学逻辑系统描述系统结构和特性，结合系统公理和推理方法实现对特性的证明过程，该方法可以实现对现实中无穷系统的描述和特性验证[8]。

工业软件工程的严格方法(Rigorous Approach to Industrial Software Engineering，RAISE)源自于缺乏模块性、不能处理并发情况的维也纳开发方法，在描述和验证系统时，可以使用“||”操作符描述并发进程，module定义可以清晰、方便地描述系统模块化结构，RAISE也可通过type、sets等更为自然地描述系统变量和实体定义，且RAISE的封装性和继承特性使得实体描述相对独立，既增强了扩展性，又降低了不兼容性，并且在系统的各个开发层次中，均可采用RAISE规范语言进行描述，进而使得整个开发过程处于同一语义框架内[9，10]。但是，该方法无法应用于带有实时性的混成系统描述中，从而严重制约了其发展，因此，对RAISE进行时间化扩展是解决问题的关键[11]。

无线闭塞中心(Radio Block Center，RBC)等级转换场景的完成与否直接影响高速列车的运行效率和安全，在对该运营过程详细分析的基础上，采用扩展后的TRSL方法实现建模，并对切换正确性和实时性进行了推理证明，通过验证系统规范对等级转换功能性和实时性的要求，为优化、完善系统规范提供可靠的理论依据，从而说明该方法的正确性和通用性，将其推广应用到整个列控系统或者更加复杂的系统中。

1　TRSL介绍

在标准的RAISE规范语言(RAISE Specification Language，RSL)中主要包括应用式、命令式和并行3种规范[12]。在应用式中，可以定义type、value和axiom，除了固有的Unit、Char、Bool等7种类型和let、case2个应用式表达式，还包括Functions、Sets、Lists、Maps定义以及各自对应操作符的应用；在命令式规范中，可以实现对用来贮存特定类型值的variable定义，而且until、for、while循环表达式，以local开始以in做以限制并以end表示结束的局部表达式，post后置表达式也包含其中；RSL提供了连接符来表述说明需要被并行计算的表达式，而且还对通信原语做了定义，使得多个需要被并行计算的表达式之间可以通过channel进行通信。通过灵活应用以上3种规范，可以实现对系统反应性、混成性以及并发性的进程描述。在RSL探究过程中，对其进行了扩展，引入一个Time类型和一个wait e表述延迟的表达式，从而形成TRSL新方法，增添了对实时性的描述机制[13]。

TRSL依赖数学逻辑来表达系统结构和验证特性，由于高铁列控系统结构复杂、规模庞大，直接使用形式化方法描述验证，不仅成本需求高，而且验证效率也会有一定程度的降低，故而引入域方法实现系统模块的划分，整个验证框架如图1所示。

图1　基于TRSL的建模验证框架

首先对系统需求规范进行抽象化处理得到系统域模型，并使用TRSL对其进行描述，得到由命题、定理等构成的TRSL模型，然后将系统特性表述为axiom形式，最后使用RAISE推理规则对模型进行验证。在验证时，根据系统性质和模型以及RAISE推理规则，不断对公理进行恒等的推理演绎，直到推出验证结果，并对结果做以分析判断。

2　RBC等级转换分析

RBC等级转换主要包含C2-C3、C3-C2以及故障降级3种情况，本文主要对前2种进行描述验证。C3/C2间的转换需要设置相应的转换点、标志牌和确认区，应答器的设置需满足高铁列控系统应答器应用原则(V2.0)中的规定，以保证列车能够在运行过程中实现不停车自动切换，具体如图2所示[14]。

2.1构建信息交互图

当列车从C2级区域进入C3级区域时，为了提高列车运行速率，需从C2转换到C3控车，主要工作包括：车载注册到无线网络、与RBC建立通信、从RBC获得行车许可(Movement Authority，MA)等步骤[15，16]。当列车驶离C3区域进入C2区域范围时，RBC根据等级转化预告点(Lever Transition Anticipation，LTA)的信息向车载下达转换预告命令，列车头部通过等级转换执行点(Lever Transition Operation，LTO)时转为C2级，尾部越过执行应答器后车载向RBC报告位置信息，随后断开与RBC的连接，注销列车信息，关闭与铁路移动通信系统GSM-R (Global System for Mobile Communications-Railway)的连接，最后按照C2级控车[17]。

根据对RBC等级转换原理的分析，可以得到转换过程中各主要设备间信息传递的交互图，如图3、图4所示。

图2　C2/C3应答器布置和确认区设置

图3　C2-C3级RBC等级转换信息交互图

图4　C3-C2级RBC等级转换信息交互图

2.2建立状态转移图

RBC等级转换过程的发生在时间上来说是连续的，但是在整个进程中设备间却是离散地传递信息，而且在执行操作以外的时间轴上，皆无连续动作的出现，从而可以将执行操作的那段时间段看成是一个连续进程，以RBC与列车车载交互时信息的传输为分界线，忽略没有操作执行的时间段，继而实现在时间上

离散化整个连续进程，最终得到RBC等级转换的状态转移图[18]，如图5所示。针对RBC等级转换，主要考虑了司机、列车、RBC和应答器4个对象，为了简化描述，将动作操作比较少的应答器和司机归于RBC和车载中，而且，对设备的每一个状态进行了编号。

在图5中，方框表示设备状态，方框内则是设备在每一个状态下需要执行的事件。随着时间的推演，设备状态不断发生变化，而状态在变化的同时要完成方框内需要执行的事件，在等级转换过程中主要是通过信息的传输来触发这些事件的发生，因而可以得出，信息的交互过程使得设备的状态随着时间的推移不断地发生变化，最后达到每个设备的最终状态，从而完成了等级转换这一个过程。

3　形式化建模

3.1建立域模型

为了降低对复杂系统建模的难度，简化后续对RBC等级转换过程的TRSL描述，引入了域方法。域是一种抽象方法，在蕴含自己本身特性的同时，也涵盖与其他域之间的联系关系，其本质是对系统实现模块化分解；域结构定义为D=(S，I，O，F(s)，T，D’)，其中，S是系统状态集合(S1，S2，…，Si)，S1代表系统初始状态；I是系统的输入集，O是输出集，而且此二集合与S相关；F(s)是系统域函数，实现从I到O的一系列操作行为，表示为F(s)=I(si)1 ×…×I(si)i→O(si)1 × …×O(si)i；T是域模型特性集合，主要体现F(s)的性质；D’子域集是一个可选项，与D有着相同的定义方式。

图5　RBC等级转换状态转移图

RBC等级转换的实质是通过车载和地面间持续不断的信息交互传递，使设备的状态不断迁移发生变化，最终实现等级的转换。将RBC等级转换过程看作是一个域，得到域结构模型如图6所示。

图6　RBC等级转换域结构模型

根据域的定义，针对RBC等级转换场景，提出输入In、输出Out和函数F三个基本元素。在In和Out中包含了车载设备和RBC的状态参数信息等，车载的等级、列车的速度和位置、轨道电路区间占用情况等均可以看作是域的In，这些信息在F的推动下，不断迁移不断变化，直至Out进入转换后的状态参数。根据前述对RBC等级转换过程的描述和分析可知，等级转换的实现是在信息交互的推动下完成的，因而，函数F的作用就相当于信息交互的进行，即整个信息交互的过程就是F函数。

3.2域模型到TRSL模型的转化

RBC等级转换域模型描述了系统的抽象静态结构，只有匹配动态行为后才可完成系统完整表述，而且域模型特性T的验证最终是要使用形式化方法TRSL来实现，因而需要实现域模型到TRSL描述的转化。

域模型元素分为非特性元组S、I、O、F(S)和特性元组T，若系统域结构模型已被搭建，系统的I、O集合不仅表示了系统的输入、输出状态，而且体现了系统的边界范围，而F就是实现此功能的要紧之处，对域非特性元组F的TRSL实现也是描述的关键。以C2-C3等级转换的RBC模块举例说明，对于域的非特性元组，状态S主要使用type定义完成，具体如下。

class

type

RBC∶Nat

/*定义了Nat类别的RBC模块*/

RBC_state==R1|R2|R3|R4|R5|R6|Rok|Rerror

/*RBC_state类型包含八种状态值*/

vh∶vehicle，r∶RBC，gr∶GSM-R

/*vh代表车载，r代表RBC，gr代表GSM-R*/

RBC_next(r，gr) ≡

/*函数RBC_next用来决定RBC的下一个状态*/

case state(r) of

/*判断RBC在哪一个状态*/

R1→R1execute-task(r，gr)

/*若RBC在R1状态时要执行R1内所有事件*/

Rok→(r，gr)，Rerror→(r，gr)

/*如果在成功或错误状态，则不发生变化*/

end

对于C2-C3等级转换的RBC模块，域的非特性元组I是指RBC_state类型中的R1状态，而O可能是顺序执行完所有状态之后的Rok状态，也可能是出现故障或未完成所有状态顺序执行的Rerror错误状态，而且，整个I到O的操作实现是由F完成的，并且，针对每一个状态，I、O以及F均有所不同体现，例如，R2状态的描述如下。

R2execute-task(r，gr) ≡

/*R2状态执行事件*/

let (news，gr)=RBC_obtain(gr) in

/*通过函数RBC_obtain(gr)获取消息*/

case news of

/*判断消息类别*/

data_train(vh，r)→RBC_transmit(Loca_req

(r，vh)，gr) || RBC_transmit(MA_req(r，vh)，gr);

/*如果r收到列车数据消息data_train(vh，r)，则向vh发送位置报告请求参数Loca_req(r，vh)并传输MA请求参数信息MA_req(r，vh)*/

wait transfernews_time; state_change(R3)

/*等待端到端传输时延后，r迁入R3状态*/

nil→(r，gr)

/*如果收到nil信息，则不发生动作*/

error→state_change(Rerror)

/*如果收到error消息，转移进入Rerror状态*/

end

在设备状态和状态间转移的表述中，使用TRSL中的“||”和“;”操作符实现对系统并发、顺序事件的描述，与此同时，利用type、value定义来对列控系统无线网络QoS指标参数[19]做以说明，具体使用时，采用wait e表达式来表述。例如，车地间连接建立的TRSL表述如下。

type

LinkB_time={t∶Time·5

value

LinkB∶vehicle×RBC×Bool

LinkB∶UnitUin any write Unit

LinkB() ≡ LinkBuild(vh，r); wait LinkB_time

对于域的特性元组T，数字特性使用“∑”、“<”、“+”等各种数学运算符将其表述成axiom形式进行规约，状态特性采用逻辑符号“^”转化成Bool类型进行识别，如下规约了C2-C3转换场景交互正确性要求和部分时间特性约束。

axiom

[correctness_C2-C3]

/*C2-C3级间转换正确性公理*/

∀vh∶vehicle，r∶RBC，gr∶GSM-R·

/*vh代表车载，r代表RBC，gr代表GSM-R*/

vehicle_state(vh)=Vh1∧RBC_state(r)=R1∧

/*定义vh和r的初始状态*/

vehicle_gain(vh，gr)=nil ∧

RBC_obtain(r，gr)=nil ∧

/*初态时信道中不存在任何信息*/

let (vh',r',gr')=Tra(vh，r，gr) in

/* Tra 是一个状态遍历函数*/

vehicle_state(vh')=Vhok∧

RBC_state(r')=Rok∧

/*在遍历条件下，达到vh、r最终态Vhok和Rok*/

TotleT1-expend (R3，Rok)<=20∧

/*车载和RBC交换数据的时间预估为20s*/

TotleT2-expend(Vh1，Vhok)<=80

/*从GSM-R注册到完成转换时的时间不大于80s*/

[realtime_C2-C3]

/*C2-C3级间转换实时性公理*/

TotleT1-expend(R3，Rok)=

/*车载和RBC交换数据的时间统计*/

TotleT2-expend(Vh1，Vhok)=

/*从GSM-R注册到完成转换时的时间统计*/

3.3RBC等级转换的验证

在RBC等级转换场景，选择了切换正确性和实时性两个典型指标。切换正确性要求判别以下2个条件：第一，按照流程系统能够进入成功状态；第二，遍历所有实例中系统状态的路径。实时性指标不仅要求系统要在确定的时间内做出响应，而且要保证响应的正确性。在该场景中，一旦违反相关时间的约束，不光会影响到行车效率，可能还会造成列车安全事故。

为了实现对RBC等级转换实时性和正确性的建模验证，首先需要使用TRSL将系统需求描述成axiom形式，完成系统特性要求的公理描述后，根据RAISE的等价规则、推断规则以及与分解等推理规则对建立的axiom模型进行推理验证，整个验证流程如图7所示。

在验证的过程中，首先定义所需的变量、状态、通道等，其次设定设备状态和通道的初始值，然后根据条件进行状态的遍历和时间的考量，最后判断结果是否符合要求。为了实现状态的迁移，使用了函数Tra来进行状态的遍历，在Tra中为了获取下一状态引入了next函数，函数Tra通过next来获取下一状态的同时也使用finished来判断是否已经达到最后状态，如果不是函数指向下一遍历对象状态继续执行Tra函数。

结合列车车载模块和RBC模块，按照图7的系统特性验证流程图，依靠Tra遍历函数借助函数next和finished，使用RAISE推理规则中的equivalence rules(等价)、and_split_inf(与分解)、inference rules(推断)等规则[20]，对C2-C3等级转换的axiom描述进行推理演绎，具体过程如下。

首先使用规则假设、与分解，将正确性公理分解为式(1)和式(2)

(1)

(2)

当式(1)的切换正确性和式(2)的实时性验证结果都为true时，才表明系统设备能够在规定的时间内实现C2到C3的转换。

对于切换正确性，使用与分解得到以下二式

(3)

(4)

只有vh和r均顺利达到成功态时才能说明能够完成转换。为了实现状态的迁移，使用了函数Tra通过next借助函数finished来执行操作遍历。

首先证明式(3)和式(4)，使用值代入规则将(vh',gr')带入Tra函数中，从而得到式(5)

Tra(vh',gr')≡let (vh',gr')=next(vh，gr) in"

(5)

else Tra(vh',gr') end

再依据函数next，使用推断值代入得式(6)

next(vh',gr')≡let(vh',gr')=vehicle_next(vh，gr)

(6)

根据axiom初始化赋值以及推断规则，等价为执行Vh1execute-task(vh，gr)，再依据推断规则，等效为执行Vh1状态内所有事件。操作结束后vh转入Ve2状态，接着使用值代入将结果代入式(5)中，依据推断规则将执行式(7)

if finished(vh',gr') then (vh',gr')

(7)

由于vh目前转入Ve2状态，未达到finished函数中定义的结束态，故而可得到式(8)

(8)

由于vh当前状态已经执行完毕，函数会指向下一遍历对象状态，即进入RBC的状态遍历。使用值代入规则将(r',gr')代入Tra函数中，得到r的Tra函数定义，再根据next函数，使用推断、值代入得到r的next函数定义。根据初始化条件，r执行RBC_next函数，使用推断规则可以等效为执行R1execute-task(r，gr)；由于Ve1状态执行中输出了消息callRBC(vh，r)，该消息又作为RBC初始化状态执行的I存在，故而等价为执行R1状态内所有事件；操作完毕后转而进入R2状态，接着使用值代入将结果代入r的Tra函数中，根据推断规则将执行finished函数，而且结果为false；由于已完成当前状态操作，函数会指向下一遍历对象状态，后续推理过程与上述类似，不再赘述，最终，可以得到式(9)和式(10)

(9)

(10)

使用值代入规则将上述两式代入式(1)中，从而得到结果：true ∧ true，该结果说明了C2-C3等级转换时，vh和r都能遍历完所有状态而达到成功态，从而证明了能够有效地完成C2-C3的转换。

实时性证明是与交互正确性验证同时进行的。根据转换需求的axiom模型，结合vh和r的TRSL表述，使用RAISE推演规则进行推导，最终可得到式(11)和式(12)

(11)

(12)

使用值代入规则将上述两式代入式(2)中，得到结果：true∧true，再结合axiom描述和式(1)的推理结果，可以得到结果恒为true值，从而证明了C2-C3等级转换过程满足系统实时性和交互正确性的需求。

C3-C2的特性验证推理过程与上述C2-C3的步骤类似，此处不再详述，最终可以得到执行结果如下

(13)

(14)

(15)

对式(13)和式(14)运用值代入规则得到结果为true值，从而说明车载和RBC借助Tra函数不断地进行状态遍历后能够进入正确状态，能够顺利地完成C3-C2的转换，即满足切换正确性要求，再结合式(15)，可以表明，列车在线路上运行时能够完成C3-C2转换，而且满足实时性的约束条件。

通过以上分析验证，证明了TRSL方法能够全面、精确、有效地对系统行为进行描述，并对系统特性实现验证，继而说明了该方法的正确性和通用性，从而为复杂系统的设计、开发和验证提供新方法和根据。

4　结论

高铁列控系统呈现出结构分布、响应快速、实时性强等多样化特性，通过分析形式化验证方法，采用基于定理证明的TRSL方法对RBC等级转换进行建模，并实现对系统模型交互正确性和实时性的验证。本文首先对RBC等级转换场景进行分析，根据转换过程中信息的传递建立了信息交互图，再将整个连续转换过程做以时间上的离散处理得到了状态迁移图，然后使用域方法建立了RBC等级转换的抽象域模型，并采用TRSL对其实现形式化描述，最后将RBC等级转换的切换正确性和实时性描述成axiom形式，结合RAISE推理准则和系统设备TRSL描述，不断推理演绎实现对切换正确性和实时性的两重验证，结果表明RBC等级转换满足系统规范对功能性和实时性的要求，从而说明该方法的有效性、正确性和通用性，为安全苛求系统的设计、开发和验证提供一种新的途径和依据。

[1]唐涛.列车运行控制系统[M].北京:中国铁道出版社，2012:168-178.

[2]赵显琼，唐涛.多端日形式化测试自动生成方法在CTCS-3车载系统中的应用[J].铁道学报，2011，33(7):44-51.

[3]IEC.IEC62425:2007. Railway Applications-Communication， Signaling and Processing Systems-Safety Related Electronic Systems for Signaling[S]. IEC. 2003.

[4]IEC.IEC61508:2005. Functional Safety of Electrical/ Electronic/Programmable Electronic Safety-Related Systems[S]. IEC.2005.

[5]吕继东.列车运行控制系统分层形式化建模与验证分析[D].北京:北京交通大学，2011:1-22.

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

[7]侯刚，周宽久，常军旺.基于时间STM的软件形式化建模与验证方法[J].软件学报，2015，26(2):223-238.

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

[9]陈怡海，缪淮扣.两种形式语言:RSL与Z的分析比较[J].计算机应用与软件，2002，19(4):11-50.

[10]贾若宇，赵保华，屈玉贵，等.CSP和RSL应用于协议形式化描述的研究[J].计算机应用，2003，23 (1):10-12.

[11]李黎.混成系统的描述和设计与Timed RAISE项目[J].计算机科学，2000，27(7):82-84.

[12]The RAISE Method Group.The RAISE Specification Language[M]. UK: Prentice Hall int. 1992:1-249.

[13]Li Li.Towards a denotational semanties of timed RSL using duration caleulus[J]. Journal of Computer Science& Technology， 2001，16(1):64-76.

[14]丁春平，陈永刚.Timed RAISE方法在列控系统等级转换场景中的应用研究[J].铁道标准设计，2015，59(8):164-169.

[15]铁道部科技司.CTCS-3级列控系统标准规范—CTCS-3级列控系统系统功能需求规范(FRS)[M].北京:中国铁道出版社,2009.

[16]Tianhua Xu， Tao Tang， Chunhai Gao， Baigen Cai. Logic verification of Collision Avoidance System in train control systems[C]∥IEEE. Intelligent Vehicles Symposium 2009. Xi’an. IEEE, 2009:918-923.

[17]王振强.CTCS-3级列控系统等级转换运营场景智能形式化研究[D].兰州:兰州交通大学，2014:1-8.

[18]Kun Wei，Jim Woodcock，Alan Burns.Modelling temporal behavior in complex systems with timebands[A]. In: Mike Hinche， Lorcan Coyle. Conquering Complexity[C]. London: Springer， 2012:277-307.

[19]中国铁路总公司.CTCS-3级列车运行控制系统[M].北京:中国铁道出版社,2013.

[20]C.George，S Prehn.The RAISE Justification Handbook[M]. LACOS/CRI/DOC/7/V5.1994.

Research on TRSL-based RBC Level Transition Scene

CHEN Yong-gang， DING Chun-ping

(School of automation and electrical engineering， Lanzhou Jiaotong University， Lanzhou 730070， China)

As a main scene of the Chinese Train Control System， RBC (Radio Block Center) level transition scene， whether it can switch successfully， will directly affect high-speed train operating efficiency and safety. By analyzing the formal verification method， the method of time-based industrial software engineering specification language of theorem proving (Timed Rigorous Approach to Industrial Software Engineering Specification Language，TRSL) is selected. On the basis of the analysis of level transition process， interactive information figure is designed， state transition diagram is constructed， TRSL descriptions of the scene are implemented combined with domain modeling method， and finally the double verification of interaction correctness and real-time capability is fulfilled by means of inference rules and associated system features. The results show the consistence of the scene with system specifications in terms of functionality and instantaneity， and demonstrate the effectiveness， accuracy and versatility of the method， which may provide a new way and basis for the design， development and validation of train control system．

Train control system; RBC level transition; TRSL; Scene interaction correctness

2016-01-19

国家自然科学基金(61164101)

陈永刚(1972—)，男，副教授，主要研究方向：交通信息工程及控制，E-mail：chenyonggang@mail.lzjtu.cn。

1004-2954(2016)08-0122-08

U284.48

ADOI:10.13238/j.issn.1004-2954.2016.08.026