高速铁路CTC分界口临时限速系统建模与验证

赵荣亮，王长林

(西南交通大学 信息科学与技术学院，成都 610031)

临时限速系统是高速铁路列车控制（简称：列控）系统的重要组成部分，临时限速的设置直接关系到列车的运行效率和运行安全。临时限速分为突发限速和有计划情况下的限速，仅在某段线路上一定的时间范围内有效，其工作流程即拟定、设置、执行、取消等具有严格的时间约束特性，是典型的实时系统。根据列车的实际运行情况，临时限速区段可能设置在调度集中系统调度台分界处，此时，临时限速系统与相邻的调度台之间都有信息交互，表现出的交互特性更加复杂。

形式化方法以数学为基础，运用严格的方法和语义对系统特性或行为进行精确描述[1]，根据描述模型，可以最大限度地验证系统的正确性。时间自动机是对自动机理论的扩展，不仅可用来描述系统的时间特性，还能很好的描述系统的交互特性。基于时间自动机理论的验证工具UPPAAL为用户提供了良好的建模仿真界面，并且能够自动对系统的属性进行验证。

本文基于时间自动机理论，应用UPPAAL建模验证工具，对CTC分界口临时限速的工作流程及信息交互过程进行仿真建模，并对系统的安全性和受限活性进行验证。

1 CTC分界口临时限速场景分析

临时限速系统的基本构成如图1所示。

图1 临时限速系统构成

临时限速的设置应满足运输安全，并要求灵活设置。当调度集中系统（CTC，Certralized Traffic Command System）分界口处由于施工、维修或自然灾害等原因需要设置临时限速时，临时限速系统不仅要完成自身临时限速的设置，还要与相邻调度台临时限速设备之间进行信息交互。临时限速在CTC分界口处的场景如图2所示。

图2 CTC分界口处临时限速场景

其中，左侧调度台命名为A,右侧调度台命名为B，对应设备均通过在其后面加上相应的字母来区分。根据站场图，标示出相邻调度台临时限速命令的拟定范围和限速数据的覆盖区域，并标示出边界TCC/RBC的单向临时限速数据覆盖区域（图中范围均为示意图）。

根据图2中的方向所示，临时限速命令的拟定责任方遵循“以线路正方向，限速起点所在局”的归属原则。图2中限速区1由CTC-A负责拟定，限速区2由CTC-B负责拟定，限速区1与限速区2均在两侧TSRS数据覆盖范围内，因此，TSRS-A数据覆盖区内限速区1的限速信息要发送给TSRS-B，同时，TSRS-B临时限速数据覆盖区内限速区2的数据也要发送给TSRS-A，使双方的限速命令同步，这样才能形成正式的临时限速命令。当出现通信中断或其它原因照成命令状态不一致，各TSRS请求刷新，进行命令状态同步，同步原则以命令发起方为准。若同步失败，则判断为故障，跨界临时限速设置不成功。各TSRS根据双方的限速结果，生成最终的限速命令。

本论文主要对分界口临时限速的拟定校验、验证、执行流程进行建模，由于临时限速的取消流程与执行流程类似，不再详细分析其工作过程。

1.1 分界口临时限速命令拟定

调度台CTC-A施工调度员负责提出跨界临时限速命令的申请，与相邻的调度台CTC-B联系确认后，拟定正式限速调度命令，下发给对应的TSRS-A进行有效性验证，并将验证结果传递给相邻的TSRS-B，请求CTC-B的TSR校验，综合两侧的校验结果，形成文本形式临时限速调度命令，送至行调台CTC-A、CTC-B，调度员确认后存入TSRS。

1.2 分界口临时限速命令激活验证

临时限速服务器TSRS-A实时检查存储的临时限速调度命令开始执行的时间，在计划开始执行前30 min向原拟定方提示激活存储的相应临时限速命令，并且每间隔10 min提示一次，直到确认或超出命令结束时间。TSRS-A激活提示检验通过后请求TSRS-B激活提示并检验（除时间信息处，其它条件均满足即可）。激活成功后由TSRS-A下达验证，并分发给相关TCC/RBC进行验证，同时请求TSRS-B分发并进行验证。

1.3 分界口临时限速命令执行

临时限速服务器TSRS-A设置提示成功，请求TSRS-B设置提示，TSRS-A综合设置提示结果，提示调度员下达执行。TSRS-A分发限速命令至相关的TCC/RBC及TSRS-B执行，TSRS-A在请求邻站执行结果的同时，告知本地执行的中间结果，综合执行的结果并送行调台显示。

2 系统建模仿真

2.1 时间自动机

时间自动机使用时钟变量表示时间，用一个约束条件来注释状态转换图，这个与时间有关的约束条件决定了状态转换的发生时机[2]。对于一个时钟变量的有穷集合X，时钟约束的集合φ(X)的形式语法为：φ：x≤c|c≤x|x

时间自动机A是一个六元组（∑, S, S0, X, I,E），其中：∑ 是一个有穷标记集合，S是一个有限状态集合， S0∈S是开始状态集合，X是一个有限时钟集合，I是一个映射，为每个位置s指定φ(X)中的一些时钟约束，E⊆S×∑×2X×φ(X)×S是转换集合，一个转换（s, s', a, λ, φ)表示在符号a下从位置s到位置s'的一条边，φ是X上的一个时钟约束，指定什么时候转换发生，集合λ⊆X指这次转换中被复位的时钟。时间自动机的语义由一个与它相关的状态转换SA来定义，SA的一个状态是一个偶对（s, v），s是A的一个位置，v是X的一个时钟约束[3]。

2.2 基于时间自动机模型

根据分界口临时限速系统的工作流程，利用UPPAAL建模仿真工具建立时间自动机模型。分界口临时限速信息交互通过4个活动对象来完成，即CTC-A、TSRS-A、TSRS-B 、CTC-B，构造出每个对象的时间自动机模型，通过自动机网络描述整个系统。构造出时间自动机依次记作 TACTC–A、TATSRS–A、TATSRS–B、TACTC–B，如图3所示。

图3 时间自动机模型

图3中，各位置之间通过同步通道实现转换的同步发生，其中，“！”结尾的标记表示发出此信号时转换发生，“？”结尾的标记表示接收到此信号时转换发生[4]。标有 C 的圆圈为坚定位置[5]，可以冻结时间即下一个转换必须无延迟的离开。规定模型中位置的命名规则：各设备模型中以“P_”开头表示限速命令拟定(prepare)过程,以“E_”开头表示TSRS中限速命令的执行下达（execute）过程，以“S_”开头表示限速命令的设置（set）过程。模型中的主要位置如表1所示。

表1 模型中的主要位置

模型中的主要通道如表2所示。

TA=TACTC–A||TATSRS–A||TACTC–B||TATSRS–B

整个时间自动机网络使用全局变量进行通信，用来保证系统逻辑功能的准确性。整型变量如confirmFlag、promptFlag、exeFlag分别用于控制确认、提示、执行结果，取值为1表示成功，0表示失败，以此来达到模型逻辑的准确性。应用时钟变量进行精确的时钟控制，设置时钟集合 X={T0, T1, T2}，其中，T0用来控制分界口临时限速命令激活验证提示时间，T1、T2用来描述相应的TSRS与TCC/RBC的通信时间。模型中T_reaction、T_timeout分别表示TSRS与TCC/RBC通信的响应时间和中断时间，由于本文主要对分界口临时限速系统信息交互进行建模，侧重于跨界限速，因此没有列出TCC/RBC的时间自动机模型，但在TSRS-A的模型中描述出了其与TCC/RBC的通信过程，同时，详细对调度台A限速命令的拟定、验证、下达过程进行建模，与调度台B有关的模型描述了辅助完成调度台A限速命令下达的过程，其与调度台A相似的工作过程，在模型中均省略。

3 系统模型验证

根据CTC分界口临时限速系统约束提出的系统功能和性能要求，利用UPPAAL工具分别对其进行验证，从而说明系统的安全性和受限活性。

系统的安全性用于描述系统不一定发生的事情，指“坏的事情永远都不会发生”，其验证可以归结为时间自动机的可达性分析；系统的受限活性用于说明系统必定会发生某些事情，指“好的事情终究会发生”[5]，可以由时间自动机位置的不变式和转换的约束条件来保证。

系统的功能和性能要求如下：

（1）功能属性要求：a.CTC应能拟定、设置、取消临时限速命令；b.TSRS保证限速命令先验证后执行；c.TSRS-A激活提示成功的同时请求相邻TSRS-B激活提示；d.TSRS-A能分发临时限速命令到相应的TCC/RBC执行同时请求TSRS-B分发执行； e.各设备均应对接收到的限速信息进行有效性验证。

（2）性能属性要求：a.TSRS-A通信响应间隔在T_reaction内完成；b.在T_timeout时间内TSRS-A通信未完成， 则视为通信中断。

UPPAAL为验证提供了一种BNF（Bac-kus Naur Form）语法：

Prop:= A[]φ|E<>φ|E[]φ|A<> →ψ其中φ,ψ为所验证的系统性质的逻辑表达式；字符A、E用来量化路径即时间自动机描述的一个转换，A表示给定的性质对于所有路径均满足，E表示至少有一条路径满足性质，[]、<>用来量化路径上的状态，[]表示路径上的所有状态均满足给定的性质，<>表示路径上至少有一个状态满足给定的性质。

应用BNF语言在UPPAAL验证器中对以上列出的性质进行验证。

把上述验证语句输入UPPAAL验证器中，逐条验证每条性质。

在验证器中，性质列表中每条性质后面的灰色圆形标志变成绿色表示验证通过，验证的进度与结果一栏中进一步表明列表中所列的性质均满足，即CTC分界口临时限速时间自动机网络 能满足系统的这些性质。通过验证说明模型是安全可靠的，系统满足逻辑和时间上的要求。

4 结束语

本文在分析CTC调度台分界口处临时限速工作流程的基础上，以其安全性和受限活性为验证目标，建立整个系统交互的时间自动机网络模型，作为验证的基础。根据CTC分界口临时限速系统约束提出功能和性能等系统性质，利用UPPAAL验证工具，验证了各条性质均得到满足，从而说明了系统的安全性和受限活性，为系统的设计和开发提供了一定的依据。

[1]古天龙.软件开发的形式化方法[M].北京:高等教育出版社，2005：5-67.

[2]吴永刚，陆慧娟.基于时间自动机的实时系统建模及验证[J].计算机时代，20116（1）：2-3.

[3]刘传会，张广泉.一种基于时间自动机网络的实时系统形式化验证方法[J].苏州大学学报，2008，24（1）：35-40.

[4]袁 磊，王俊峰.CTCS-3级列控系统临时限速建模与验证[J].西南交通大学学报，2013，48（4）：710-712.

[5]OLDEROGER, DIERKSH. Real-time systems[M].London:Cambridge University Press，2008: 137-146．

[6]康仁伟.基于时间自动机的CTCS-3级列控系统建模方法与验证研究[D].北京:北京交通大学， 2013：40-53.