基于Timed-UML顺序图的RBC交接形式化建模与分析

安　越，李国宁

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



基于Timed-UML顺序图的RBC交接形式化建模与分析

安越，李国宁

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

摘要：在CTCS-3级列控系统中，采用RBC技术将线路划分成多个管辖区段。当列车行驶并跨越相邻RBC交界区域时，控制权将会移交至前方相邻RBC，整个过程称为RBC交接。在运行中，RBC交接过程能否实时安全可靠地执行，直接影响着列车的行车效率和乘客的生命安全。采用一种基于添加实时约束的UML顺序图与时间自动机结合的模型来建立RBC交接场景。以双车载电台的RBC切换策略出发，建立切换的Timed-UML顺序图模型，然后按照UML-TA转换规则，建立得到完整的时间自动机网络模型。并利用UPPAAL验证工具对RBC交接模型进行形式化建模及分析，对模型的死锁和功能实现做了验证，从而达到对CTCS-3级RBC子系统的实时性以及设计规范合理性的验证目的。

关键词：车载系统；RBC交接；实时UML顺序图；时间自动机

1概述

RBC子系统作为CTCS-3级列控系统车-地数据信息交互中心，主要负责给列车发送行车控制所需的数据信息，包括移动授权MA(Move Authority)及线路信息等。车载子系统根据接收到MA数据，结合列车当前所在的位置，计算距离-速度监控曲线，对列车的运行状态实时监控，保证行车安全。RBC交接是CTCS-3级列车控制系统非常重要的运行场景之一，在整个交接过程中主要是由两个相邻RBC系统以及车载之间的数据信息的交互来完成。

根据RBC切换的功能要求，从数据的传输到切换功能的实现，必须满足数据及其交互的一致性，实时性和安全性要求，采用形式化建模与验证方法是可行的。形式化模型方法具有严格的数学语法和语义，可以准确地描述系统模型，但其所包含的复杂数学理论很大程度上限制了工程人员的学习和使用[1]。在工程实践中，人们更多地倾向于使用统一建模语言UML来建模和交流，但对于实时性系统来说，UML的建模能力有限。

时间自动机TA(Timed Automata)是在自动机理论的基础上扩展时间约束，为了解决实时系统建模和验证问题，它提供了一种简单而有效的方法以描述带有时间因素的系统，为实时系统的行为建模和性能分析提供了形式化模型[2]。为了实现自动模拟和分析实时系统的行为特性，有学者在时间自动机原理的基础上开发了一种模型检测工具UPPAAL。该验证工具采用带有整型变量的TA网络模拟实时系统的行为，采用时序逻辑TCTL(Time Computation Tree Logic)刻画系统的实时特性，然后将二者载入验证器中，通过有限状态搜索验证系统是否具备所期望的性质。

根据RBC切换功能有着严格的实时性等特征，本文结合了UML和时间自动机(TA)的优点，在UML2.0的基础上，将UML顺序图扩展了时间机制，并建立了RBC切换模型，然后将UML顺序图转化成相应的TA网络模型；并通过UPPAAL验证工具对RBC切换的TA模型进行形式化验证和分析[3-4]。

2基于UML扩展模型的建模

UML时序图是强调信息时间顺序的交互图，它描述了对象之间消息传送的时间顺序，并按照时间顺序对系统控制进行建模，是系统的动态试图，强调了对象间发送信息的顺序和交互，显示的是对象间的动态转化和合作关系[5-6]。

但是在模拟实时系统时，无法精确地表示很多消息传递时间或者事件间隔的时间长短，只能简单的表述事件或者消息的先后关系，这使得模型并不能全面地体现系统的实时性能。UML2.0中实现了对于实时系统的时间扩展，提供了表示时间、时间间隔约束以及用来观测时间进展的动作的原模型，这使得可以利用此机制对模型进行精确地建模。具体实例操作如图1所示。

图1　UML顺序图中的时间机制

为了使扩充的顺序图能够表达实时性并体现RBC交接中涉及的各设备间的独立时钟以及体现数据老化时间概念，对顺序图进行了一下扩展。

(1)事件上的标签值添加两个时间约束：

①时间重复；

②事件上发生对象的独立时钟时间。

(2)事件中的时间约束是表示在事件发生时必须满足的条件约束。在满足条件的时刻，系统就会转移到下个事件。

(3)当只有在满足相应的时间约束时，事件中的消息传递才能发生。

(4)根据UML2.0的时间机制，对象的每两个事件进行老化时间赋值。

3时间自动机的转换机制

在RBC交接过程中，车载系统需要处理的数据有：自身计算得到的列车所在的位置信息，以及从接口得到的RBC设备发送的MA数据和与RBC系统的通信信息。随着列车运行，这些数据信息会实时和动态地产生。根据动态数据中存在的依赖关系和数据老化特点，提出了基于TA模型的数据安全验证方法，以UML为源模型，进行了时间上的扩展，并以模型间转换规则为基础，将 UML顺序图 建立的时序模型转换为TA扩展模型并进行验证，解决了车-地动态数据存在的一致性问题和数据在应用过程中出现的组合错误等问题，并通过具体实例表明模型间转换的可行性[7]。

3.1时间自动机扩展

根据标准定义，时间自动机自带的时间的约束功能已经很好地体现了实时系统的一些时间方面的要求。但是标准的时间自动机并没有老化时间的概念，从而也无法体现老化时间对于系统的影响，所以需要在原有的模型上添加老化时间集合[8]。

扩展的时间自动机定义:时间自动机TA是一个七元组

其中：

(1)S是有穷位置集合；

(2)是初始位置集合；

(3)是有穷事件集合；

(4)X是有穷时钟集合，I是一个映射(它给每个位置S指定了一个时钟约束)；

(5)DA是老化时间集合；

(6)E∈L×∑×φ(X)×2X×DA，为状态转移集合。

TA的一种状态迁移公式为，更加直观的表示是，这个转移公式表示在事件 α(α∈∑) 发生的条件下，当事件α的发生时间满足时钟约束δ时，TA从状态n迁移到状态m，成功迁移之后，λ内部的全部时钟重新设置为0，之后从状态发生迁移的这一时刻起重新计算时间[9-10]。见图2。

图2　TA的状态转移

3.2UML-TA场景模型转换规则

规则一：单元片段转化。

为了得到相应的单元自动机，需要将每个单元片段的数据集合进行对应转化。

自动机集合S的格式为(W，da，T)的有限状态集，其中有满足R中所定义的可视事件对。da集合是时间W上的老化时间单元。对于同一对象的可视化事件对，先发生的da为时间min，后发生的时间为max，对应于UML图中的老化时间；T集合是事件上的时钟集，对应于UML时序图中对象间发生事件的时间约束条件。

规则二：组合片段转化。

UML2.0中有alt，opt，loop等组合约束片段，以及多个组合片段组成一个完整的组合，在UML中组合片段是严格按照生命线上的顺序执行，将上述这些不同的组合片段分别进行转化，得到相应的TA模型。

(1)Alt片段表示在一组行为中根据特定的条件选择交互，模型为if…else。

设函数Alt(G，A)，A代表所有可以选择片段集合，G代表对应可选分支的约束。根据Alt片段的逻辑定义，构造的TA模型为TAn(N，n0，L)。TA1，TA2，…是可选片段各自构造的自动机，从相应的UML-TA转换规则得到：

Alt(G，A)→TAalt(N，n0，L)

n0是一个新的空状态，N={n0}∪N1∪N2… ，L={，}…∪L1∪L2…。

(2)Opt片段表示单独选择，模型为switch；

设函数Opt(S)，S代表单个分支片段。TA1，TA2是各自构造的自动机，相应的转换规则：

Opt(S)→TAopt(N，n0，L)

n0是一个是新的空状态，N={n0}∪N1∪N2，L={，}∪L1∪L2。

(3)Par片段支持多个片段并发执行，执行顺序没有特定要求。

设函数Par(PF，n)，PF表示组合中包含多个片段，n表示组合中的片段个数。TA1，TA2…是多个片段组合各自构造的自动机，按照以下转换规则得到相应的自动机结构

Par(F，n)→TApar(N，n0，L)

n0是一个新的空状态，N={n0}∪N1∪N2… ，L={，…}∪L1∪L2…|{

n1，0>，…}∪L1∪L2…|…，其中S1，S2…是等概率发生事件，每个并行片段发生概率都是1/n。

(4)Loop片段表示交互片段会被循环执行。

设函数Loop(LF，guard)，LF为所要重复的子片段，guard为条件，TA是需要循环片段构造的自动机，按照以下规则得到对应的自动机

Loop(LF，guard)→TAloop(N，n0，L)

n0是一个新的空状态，N={n0，ne}∪N1，ne是一个新的空状态L={，}∪L1。

(5)Strict片段表示一组片段执行的次序有特定要求。

设函数Strict(SF，SForder)，SF为多个片段集合，SForder为片段排列顺序。TA1，TA2，…是多个片段组合各自构造的自动机，按照以下规则得到相应的自动机结构

Strict(SF，SForder)→TAstrict(N，n0，L)

4RBC交接场景的形式化建模

4.1RBC切换协议

RBC交接采用的是车载EVC和相邻RBC之间交互通信的方式实现RBC交接数据信息的交互，并且使用的RBC负责与前方相邻RBC在设定的两交界区域完成列车的无缝交接[11-12]。在交接过程中，不仅要实现自动执行交接，而且不能引起列车制动。

RBC交接有两种实现策略，包括车载单电台模式和车载双电台模式。本文以双电台的交接策略为实例进行分析，整个执行流程如下。

当列车行驶靠近两个RBC边界，并到达预告应答器组LTA时，车载设备给“YRBC”发送列车位置数据信息(msg136)。当“YRBC”收到列车位置信息后，会给车载EVC传送切换命令信息(msg201)，并将车载的ID信息和当前位置信息等数据发送给“HRBC”；车载再依据RBC提供的ID建立起和“HRBC”设备的通信，并给“HRBC”发送列车的基本数据信息；“YRBC”给“HRBC”发送列车移交预告和进路请求数据信息，并且依据获得的进路信息、“HRBC”的答复信息和线路状况数据信息计算得到包括了RBC交界的移动授权MA；车载系统依据RBC提供的ID，使用2号电台呼叫“HRBC”，呼叫成功后，建立通信。当列车的最大安全前端行驶过RBC交界处后，车载系统给相邻的两个RBC发送列车的位置信息，当“YRBC”获得列车的位置信息后，给“HRBC”发送列车已进入其所管辖线路的信息的通知；当“HRBC”接收到位置信息并检测到列车最大安全前端已经通过了RBC间的边界区域后，则给“YRBC”发送控制权接收的信息；当列车最小安全末端穿越过RBC交界后，车载系统不再接收任何由“YRBC”发送的命令信息，除了“断链命令”命令；当整个列车通过RBC交界区域后，“YRBC”向车载系统发送停止会话命令信息，车载系统成功收到这个命令后切断与YRBC的信息交互连接[13-14]。

4.2RBC切换的UML顺序图

以CTCS-3级列控系统总体技术方案内容为理论基础，并以车载双电台切换策略为实例，根据UML顺序图的扩展时间机制，对整个交接流程进行可视化建模，如图4所示。

图4　带有时间扩展的RBC 切换顺序

4.3RBC切换的TA模型

本文通过UPPAAL工具对RBC交接场景进行建模，并根据TA网络积的概念，建立相应的TA模型：EVC||HRBC||TRBC。其部分模型如图5所示。

图5　RBC切换TA图

模型中，以“!”标记的同步通道表示发出此信号时状态发生迁移；以“？”为后缀的同步通道表示接收到该条件时状态发生迁移。除此之外，定义了一些成员函数和局部变量来表示系统模型的属性和行为，在整个模型与系统之间还设置了全局变量来保证模型逻辑功能的正确性。见表1和表2。

在时间控制方面，Tevc代表车载子系统EVC的内部时钟，Tacc代表接受RBC的内部时钟，Thov代表移交RBC系统的内部时钟，它们分别对各个TA模型网络的状态运行进行记录。在状态标识中，标有U的状态为紧迫位置，没有延迟时间，从而减小整个模型中的时钟数量，从而降低了模型分析的复杂度，标有C的状态代表紧急状态，利用其的不允许下一个转移有时间上的延迟的特性，可以实现车载设备和RBC系统之间的无延迟时间数据交互[14]。模型中还设定了一些常整数rbcCycle表示RBC的数据处理时间；evcCycle表示车载EVC的数据处理时间；LTA2RN表示从交接预告应答器组到交接边界的长度距离。

表1　模型中的主要同步通道

表2　模型中的主要变量定义

5模型的验证分析

UPPAAL工具利用了时序逻辑公式在TA网络中进行有穷搜索来完成对功能的验证，该软件使用的是时间分支时序逻辑的子集，可以准确的描述线性时序逻辑[13]。BNF语法公式为

Prop::=A[]p|E<>p|E[]p|A<>p|P→p

其中：

1)E<>p表示Possible; E<>p为真，当且仅当在转换系统中存在一个序列s0→s1→…→sn，使得s0是初始状态，sn代表目标状态；

2)A[]p表示Invariantly，等价于not E<>not p；

3)E[]p表示Potentially always，E[]p为真，当且仅当存在一个序列s0→s1→…→si→…使得p在所有状态 si中都有效，并且这个序列无穷或者在状态sn终止；

4)A<>p表示Eventually，等价于notE[]p；

5)P→p表示Lead to ，等价于A[](P imply A<>p)。

并且利用BNF语法表达的时态逻辑公式能够准确的描述并发系统的性质，比如受限活性和安全性[15]。接下来将从功能逻辑、安全性和实时性对RBC切换的TA网络模型进行验证和结果分析。

逻辑功能和安全性验证。

a)A[]not deadlock，表示系统没有死锁；

b)E<>(EVC.wait4MA)and s>=aFirstMA，表示列车能够发送申请MA请求；

c)E<>(EVC.gotMA)and((hovRBC.stMA2)or (hovRBC.stMA))，表示列车能够接受MA；

d)(checkCount()==1)and(not accRBC.ConEsted)->EVC.abortion，表示安全建链失败下放弃RBC切换；

e)A<> (EVC.headOverRN)and s>=LTA2RN，表示车头越过RN能够发出关键位置报告；

f)A<>(EVC.tailOverRN)and s>=(LTA2RN+LENGTH_T)，表示车尾越过RN能够发出关键位置报告；

g)A<>EVC.headOverRN imply(hovRBC.gotLocationReport or hovQueue.hcatchMAX)，表示移交RBC总能收到头车过RN的位置报告；

h)A<>EVC.tailOverRN imply(hovRBC.gotLocationReport2 or hovRBC.joint7 or hovQueue.HcatchM-IN2)，表示RBC总能收到车尾过RN的位置报告；

i)E<>(accRBC.ready4Data)and >=aFirstMA，表示接管RBC能够收到线路请求；

j)A<>(accRBC.stTransmit1 or ccRBC.joint2) imply(accQueue.acatchTransmit1 or accRBC.gothovL-

Report or accRBC.joint1 or accRBC.gotMARes)，表示总能收到来自移交RBC的MSG136MAX的转发；

k)A<>(accRBC.stTransmit2 or ccRBC.joint3) imply(accQueue.acatchTransmit1 or accRBC.gotTrans-

mit2 or accRBC.joint6 or accRBC.endacc)，表示总能收到来自移交RBC的MSG136MAX的转发；

l) A<>((hovRBC.gotLocationReportReport or hovQueue.hcatchMAX)and accQueue.acatchMAX)

imply BREAK==1，表示未与接管RBC建立通信会晤即跨越RN时必须制动。

6结语

本文以车载双电台的模式为实例，对CTCS-3级列控系统运行场景之一的RBC交接进行分析，对其过程的实现原理，逻辑功能和实时性以及安全性进行了形式化建模和验证分析。文中利用一种将扩展了时间约束的UML顺序图和扩展了老化时间的TA模型相结合的方法对基于车载双电台的RBC交接场景进行分析，并使用UPPAAL检验工具对交接场景建立了相应的TA网络模型，然后对模型进行了完整的形式化验证和结果分析。通过文中的方法和操作，完整地验证和分析了整个RBC交接过程中的实时性、逻辑功能

等安全性能，并得到理想的结果，从而保证了CTCS-3级列车控制系统中车载子系统和RBC间的数据信息通信的安全及畅通。

参考文献：

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

[2]韩德帅，杨启亮，邢建春.一种软件自适应UML 建模及其形式化验证方法[J].软件学报，2015，26(4)：730-746.

[3]姬莉霞，马建红.基于时间自动机UML模型转换与验证研究[J].郑州大学学报(理学版)，2013，1(45)：50-55.

[4]吴永刚，陆慧娟，程倬，等.基于时间自动机的实时系统建模及验证[J].计算机时代，2011，6：1-3.

[5]黄友能.城轨CBTC系统数据的安全处理与验证方法研究[D].北京：北京交通大学，2014.

[6]周清雷，姬莉霞，王艳梅.基于UPPAAL的实时系统模型验证[J].计算机应用，2004，24(9)：130.

[7]刘传会.基于UML2.0的实时软件动态行为模型一致性验证[D].苏州：苏州大学，2008.

[8]李岩.可调整时间自动机可达性算法的研究[J].信息技术，2014(9)：4-7.

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

[10]李波，杨弘平，吕海华，等.UML2基础、建模与设计实践[M].北京：清华大学出版社，2014.

[11]丛新宇，虞慧群.基于实时UML顺序图的物联网交互模型[J].计算机科学，2014，11(14)：79-87.

[12]铁道部科技司.CTCS-3级列控系统标准规范系统-无线闭塞技术规范[M].北京：中国铁道出版社，2008.

[13]徐世泽，肖蒙.基于Timed RAISE的高速列车RBC切换协议形式化建模及验证[J].铁道标准设计，2015,59(6):138-143.

[14]唐涛，赵林，徐田华，等.基于模型的列车运行控制系统设计与验证方法[M].北京：中国铁道出版社，2014.

[15]胡雪莲，陶彩霞.基于MSC与UPPAAL的列控系统等级转换场景形式化验证[J].铁道标准设计，2015，59(2):122-127.

收稿日期：2015-09-16； 修回日期：2015-10-23

作者简介：安越(1987—)，男，硕士研究生，研究方向为高速铁路计算机技术的应用，E-mail：feixuerenzhe2377@163.com。

文章编号：1004-2954(2016)06-0132-06

中图分类号：U284.48

文献标识码：A

DOI:10.13238/j.issn.1004-2954.2016.06.027

Formal Modeling and Analysis of RBC Handover Based on Timed UML Sequence Diagram

AN Yue，LI Guo-ning

(School of Automatization & Electric Engineering，Lanzhou Jiaotong University，Lanzhou 730070，China)

Abstract：In the CTCS-3 level train control system，a line is divided into several RBC control sections. When the train runs through an adjacent RBC region，the control of the train will be handed over to the region，which is called RBC handover. In the operation of the train，safe and reliable RBC handover is the key to the operation efficiency and safety of passengers. In this paper，a model based on the combination of the UML sequence diagram with the time automaton with real-time constraints is used to establish RBC handover scenario. Based on RBC switching strategy of dual onboard radio station，the timed-UML sequence diagram model is established，and then the complete time automaton network model is established according to the UML-TA conversion rule. The UPPAAL verification tool is used to model and analyze RBC handover. The deadlock and the function realization of RBC handover model are verified to confirm the real-time performance and the rationality of the design specifications for CTCS-3 level control system．

Key words：On-board system; RBC handover; Timed UML sequence diagram; Time automaton