移动授权的形式化建模与验证

贺欢欢，陈永刚，罗雅允，张彩珍

(1.兰州交通大学自动化与电气工程学院，兰州 730070;2.兰州交通大学电子与信息工程学院，兰州 730070)

移动授权的形式化建模与验证

贺欢欢1，陈永刚1，罗雅允1，张彩珍2

(1.兰州交通大学自动化与电气工程学院，兰州 730070;2.兰州交通大学电子与信息工程学院，兰州 730070)

基于通信的列车运行控制系统(Communications-Based Train Control System， CBTC)相较于传统的基于轨道的列车运行控制系统，无论是从功能方面还是性能方面都有了很大的改进。在系统的研发过程中，对其进行建模和验证，能够发现系统设计的缺陷，进而保证系统的安全性和功能性。移动授权(Movement Authority， MA) 是CBTC系统的核心功能，用来保证列车的安全运行间隔。通过对移动授权生成原理的研究，采用时间自动机和其自动验证工具UPPAAL对其进行建模以及验证，验证结果表明，搭建的移动授权模型能够达到规定的安全要求和功能要求。因此UPPAAL能够对复杂的实时系统进行仿真验证。

CBTC；MA；时间自动机；UPPAAL

基于通信的列车运行控制系统CBTC相较于传统的基于轨道的列车运行控制系统具有安全性高、线路运输能力大、实时性好和轨旁设备少等优点。世界上主要的经济发达国家已经相继研发出了自己的基于通信的列控系统，并且已经趋于成熟。而我国CBTC系统的开发还处于初步阶段，移动授权的生成是联系CBTC系统中各子系统的纽带，并且直接影响行车效率和行车安全。采用形式化方法时间自动机对移动授权进行建模，并利用其自动验证工具UPPAAL对模型的功能性能和安全性能进行验证。

1 时间自动机与UPPAAL

时间自动机是一种形式化的建模方法，相较于有限自动机，它在模型的进程迁移间增加了时钟约束。时间自动机模型由有限个控制位置和实数型时钟构成，只有当控制位置间的时钟约束满足条件才能发生转换。基于时间自动机模型已经开发出了多种自动验证工具，经过对比发现由Aalborg大学和Uppsala大学于1995年共同开发的UPPAAL验证工具更为优越。

UPPAAL工具主要由系统编辑器、模拟器和验证器3个部分组成。编辑器用于创建和编辑要分析的系统，一个系统被描述为一系列过程模板、一些全局声明、过程分配和一个系统定义。模拟器用于检查所建模型可能的执行是否有错，以此在验证前发现一些错误。验证器通过快速搜索系统的状态空间来检查时钟约束和活性。UPPAAL还专门为模型验证提供了一种BNF语法：Prop::=A[]p|E<>p|E[]p |A<>p|p→p。这种语法的含义如表1所示。

表1 BNF语法的含义

2 移动授权生成原理分析

CBTC系统主要由区域控制器(Zone Control， ZC)、车载控制器(Vehicle On Board Controller， VOBC)、计算机联锁(Computer Interlocking， CI)、列车自动监控系统(Automatic Train Supervision， ATS)、数据库存储单元(Database Storage Unit， DSU)和数据通信系统(Data Communication System， DCS)等组成。ZC作为CBTC系统重要的轨旁部件，根据CBTC其他子系统发送的各种状态信息，为处于其管辖范围内的列车分配移动授权，并通过DCS发送给列车，以此控制列车的安全运行。

IEEE1474.1将移动授权定义为：移动授权是为在一个给定的方向行驶的列车提供权限，使其进入或通过某一特殊的轨道区段，移动授权的分配、监督和执行由CBTC系统完成，该系统实现列车的安全分隔并通过联锁为列车提供防护[2]。实质上MA是指从列车的车尾起到列车前方第一个障碍物的这部分线路，ZC每次为列车计算授权时，需要明确授权起点、授权终点和授权方向3个要素，移动授权示意如图1所示。

图1 移动授权示意

MA的生成是通过CBTC系统中各个子系统间的信息交互实现的[3-5]。图2为CBTC子系统的信息交互图。

图2 CBTC子系统信息交互

3 移动授权的自动机模型及验证

3.1 移动授权过程分析

为了简化模型，根据列车正常运行的过程，ZC可以把列车分为以下几种状态：未登录状态、登录状态、进入控制状态、正常运行状态以及注销状态[6]。在初始情况下，列车处于未登录状态，ZC通过VOBC发送给它的登陆申请来确定列车是否进入它的管辖范围，如果ZC收到VOBC发送的登陆申请，则列车的状态由未登陆状态转为登录状态；然后列车向ZC发送进入控制的申请，此时ZC需要判断CI是否为列车排出进路，如果排出则进入正常运行状态，否则列车保持在进入控制状态不变；列车在进入正常运行状态之后，则会按照ZC为它分配的移动授权运行；当列车接近ZC控制区域的尽头时，会向ZC发送注销请求信息，请求退出ZC控制，列车状态转为注销状态。一般情况下，列车只有在正常运行状态才可以要求ZC为其发送移动授权[7]。移动授权的生成一般分为3个阶段：第一为数据准备阶段，ZC周期性的刷新从其他子系统发送的各种状态信息，主要包括列车的位置信息以及障碍物的状态信息；第二为移动授权生成阶段，即对接收来的这些状态信息进行一定的预处理，生成移动授权的过程可以分为两个步骤，分别是障碍物的准备和障碍物的遍历；第三为发送阶段，即把生成的移动授权以及移动授权范围内的障碍物信息通过DSU发送给列车。

移动授权生成的流程如图3所示[8-10]。

图3 移动授权生成流程

3.2 移动授权生成的自动机模型

通过对生成移动授权重要部件ZC的分析可知，ZC要实现移动授权的分配需要对ZC与其他子系统的信息交互、对列车各个状态进行管理和移动授权生成3部分进行建模，而ZC与其他子系统的交互又分为与ATS的交互、与DSU的交互、与CI的交互和与VOBC的交互。

模型中主要位置如表2所示。

表2 模型中的主要位置

通过对以上5个部分进行建模，得到移动授权生成的成员自动机模型如图4(a)～图4(e)所示，分别为：列车、区域控制器、ZC与ATS信息交互、ZC与VOBC信息交互和ZC与CI信息交互。则整个系统的时间自动机模型为这些成员自动机模型之积，这是通过构造同步管道来实现的，用“!”结尾的通道表示发出此信息时转换发生，用“？”结尾的通道表示接收到此信息时转换发生，以此保证各成员自动机中相同的转换同步。除了同步管道，UPPAAL中还另外增加了紧迫管道(urgent channel)、紧迫位置(urgent location)和坚定位置(committed location)。紧迫管道即当这个转换发生时，没有时间延迟，它对应的转换上不能有时钟约束。在紧迫位置处没有时间延迟，理论上，它是增加了一个x<=0的时钟约束。像紧迫位置一样，坚定位置处也没有时间延迟，但必须要有一个离开坚定位置的转换[11-13]。

图4 移动授权生成的时间自动机网络模型

3.3 模型的仿真和验证

在UPPAAL的编辑器中建立好移动授权的时间自动机网络模型后，在模拟器中，对列车在运行过程中，会经历未登录、数据库版本检查、登陆、受控，正常运行和注销这几种状态的转换进行了模拟，同时在整个转换过程中区域控制子系统完成了MA发送以及与其他子系统进行了状态信息的交换。最后在UPPAAL的验证器中，应用BNF语法对ZC的性能和功能要求进行描述验证验证结果如图5所示。

图5 性质验证

(1) A []not deadlock通过验证，即系统无死锁；

(2)E<>((Train.Login)or(Train.Versioncheck) or (Train.Controlling) or (Train.Logoff))通过验证，即列车能够完成登陆，版本检查，受控和注销；

(3) E <> ZC. MAOutput通过验证，即区域控制器能够输出MA信息；

(4) A []((Train.Login imply Train. T1<=T) or (Train. Controlling imply Train. T1<=T))通过验证，即列车能够在T个单位时间内完成登陆和受控。

4 结语

本文采用形式化方法时间自动机对移动授权进行建模并应用其自动验证工具UPPAAL进行模拟验证。成功的验证了移动授权生成功能，保证了系统的活性完备性以及正确性，完成了对所建立模型的确认。因此，UPPAAL能够对实时系统进行模拟验证。

[1] 许丹.基于时间自动机的实时系统形式化建模与验证[D].苏州：苏州大学， 2007.

[2] Rail Transit Vehicle Interface Standards Committee of the IEEE Vehicular Technology Society， IEEE Std 1474.1TM-1999，IEEE Standard for Communications-Based Train Control(CBTC) Performance and Functional Requirements[S]. USA: The Institute of Electrical and Electronics Eigineers，2005：1-20.

[3] 王莉莉，张玉平.城市轨道交通CBTC系统移动授权计算的研究[J].成都电子机械高等专科学校学报，2012，15(1):32-35.

[4] Wu Dong Yong， Zhang Yong. Researching Colored Petri nets Model of Communication Based Train Control System[J]. Journal of System Simulation， 2005，17(10):23-30.

[5] 李凤华.城市轨道交通CBTC系统区域控制器的研究与仿真[D].兰州：兰州交通大学，2011.

[6] 刘晓娟，张雁鹏，李凤华.基于通信的列车控制系统移动授权的研究与仿真[J].城市轨道交通研究， 2011，12(15):48-50.

[7] Meyer zu Horste， Michael Schnieder Eckehard. Modelling and Simulation of Train Control System Using Petri Nets[J]. World Congress on Formal Methods in the Development of Computing Science l709. Berlin: Springer， FME， September 1999， 2006.

[8] 朱光文.地铁信号系统中车-地无线通信传输的抗干扰研究[J].铁道标准设计，2012(8)：112-115.

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

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

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

[12]王淳.基于UPPAAL的系统建模验证研究及其在CTCS-3列控系统的应用[D].北京：北京交通大学，2011.

[13]赵晓峰.基于螺旋模型的无线CBTC信号系统项目[J].铁道标准设计，2012(9)：98-101.

Movement Authority Formal Modeling and Verification

HE Huan-huan1， CHEN Yong-gang1， LUO Ya-yun1， ZHANG Cai-zhen2

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

Compared with the traditional train control system， the communications-based train control system has been greatly improved either in function or in performance. In the development process of the system， system design flaws can be identified by modeling and verification so that the security and functionality of the system is guaranteed. Movement authority is a core function of CBTC system and is used to ensure the safe train interval. This paper， in the light of the generation principle of movement authority， uses timed automation modeling and UPPAAL verification for MA. The verification results show that the movement authority model so established can meet the requirements for safety and function. Thus， UPPAAL is capable of simulation and verification for complex real-time systems.

CBTC; MA; Timed Automation; UPPAAL

2014-05-29；

2014-06-10

甘肃省高校基本科研项目(620027)

贺欢欢(1990—)，女，硕士研究生。

1004-2954(2015)03-0118-04

U283

A

10.13238/j.issn.1004-2954.2015.03.028