列控系统等级转换的建模研究

杨璐 陶汉卿

摘要：等级转换是高速铁路列车运行控制系统的一个主要运营场景。当列车通过CTCS-3级区域和CTCS-2级区域边界时，车载子系统、无线闭塞中心、司机、预告应答器以及转换应答器之间存在大量的信息交互过程，并对列车的安全运行和行车效率有直接的影响，因此有必要采取形式化建模方式对该过程进行分析和验证。文章根据时间自动机理论对CTCS-3级向CTCS-2级转换的过程进行建模，并应用UPPAAL对转换过程各子系统的信息交互一致性和实时性进行验证。结果表明，该过程满足交互一致性和实时性的规范要求。

关键词：等级转换;时间自动机;UPPAAL;实时性

0 引言

中国列车运行控制系统CTCS（Chinese Train Control Systm）按其地面设备、车载设备配置和功能共分为5个等级[1]，即CTCS-0～CTCS-4。CTCS-3级列控系统通过GSM-R实现车-地无线大容量通信，利用RBC子系统计算获得的移动授权以及其他的控车信息实现高速铁路列车安全、高效运行。C3级列控系统采用分布式结构，具有连续式响应和实时性强的特点，采取有效的方法实现系统特性的描述和验证已成为C3级列控系统的一项重要研究领域[2]。系统规范作为列控系统设计开发的起点和基础，一旦其存在潜在缺陷，很可能会对运营列车的安全运行带来风险[3]。因此，在C3级列控系统研发过程中对其各个场景进行建模、仿真和验证，发现系统潜在缺陷，提高系统安全性，辅助系统开发，提高开发效率显得尤为重要。列车跨越CTCS-3级区域和CTCS-2级区域边界过程作为高速铁路动车组列车运行过程的一个很重要的环节，是保障动车组安全运行和提高行车效率的基础。因而，当列车跨越CTCS-3级区域和CTCS-2级区域边界点时，针对C3向C2交接控车权并控制列车正常运行的建模研究就显得尤为重要。

CTCS-3级列控系统作为一个典型的安全苛求系统和实时系统，根据国际电工委员会标准（IEC624425和IEC61508），针对高安全苛求系统，可通过形式化方法进行建模和验证[4-5]。面向对象的同一建模语言（Unified Modeling Language，UML）具有较强的交互流程描述能力，且易于使用。文献[6]作者采用UML方法对CTCS-1级列控系统的车载ATP进行建模，并采用计算机语言编程的方法进行了验证。不难看出UML方法缺乏相应的验证工具，无法直接实现模型验证，不利于错误的有效定位。相比UML，时间自动机有其对应的验证平台UPPAAL，且UPPAAL工具平台的模型验证功能自动化程度高，当系统不满足给定的性质时，在模拟器窗口可以实现对验证错误的有效定位。因此，本文根据时间自动机理论对列车跨越CTCS-3级区域和CTCS-2级区域分界点时的等级转换功能进行研究，建立了转换过程中的列车模型、无线闭塞中心模型、预告应答器模型、切换应答器模型以及司机模型，基于该模型，对CTCS-3级转CTCS-2级的功能进行验证。

1 C3向C2转换过程分析

当线路上运行的列车即将离开CTCS-3级管辖区域并驶入CTCS-2级管辖范围区域时，RBC将根据距离转换点前一定距离处设置的等级转换预告应答器LTA的预告信息，向车载控制器发送等级转换的预告命令[7]。列车继续运行至距离等级转换执行应答器LTO一定距离时，向司机申请转换确认。当列车运行至前端通过转换执行应答器LTO时，RBC根据LTO的转换执行信息，向车载控制器发送转换执行命令。当列车完全通过转换点后，车载控制器与RBC结束通信。详见图1。

2 建立C3转C2的信息交互图

通过对列车从CTCS-3级管辖范围驶入CTCS-2级管辖范围的过程分析，可将车载控制器由CTCS-3级转换为CTCS-2级，司机、RBC、预告应答器LTA以及执行应答器LTO之间的信息交互过程简化为3个阶段（见图2）：

C3转C2预告阶段：列车正常运行在CTCS-3级线路上时，RBC为列车提供行车许可。当列车进入等级转换区，运行至等级转换预告应答器LTA，接收转换预告信息，RBC向列车下达转换预告命令。此时车载控制器根据命令激活CTCS-2级控制单元，进行实际运行速度与C2允许速度比较过程。

C3转C2等级转换执行阶段：當列车继续运行至前端通过转换点LTO时，执行转换命令，列车自动转至CTCS-2级控车。若之前司机未进行转换确认，当车载转入C2控车后的5 s内允许司机继续进行确认[8]。

列车尾部通过转换点，结束与RBC通信阶段：当列车继续运行至尾部通过转换点LTO后，车载控制器与RBC断开连接，结束通信。

3 列车跨越C3-C2分界点的等级转换模型

3.1 UPPAAL工具

1995年，Aalborg大学和Uppsala大学联合提出UPPAAL，可以通过时间自动机子模型来描述各个子系统的属性和行为，多个单独的子模型组成整个系统完整的时间自动机网络模型。通过UPPAAL平台下的模拟器窗口可以准确对其错误的路径进行定位，从而修正模型。UPPAAL验证平台为系统规范的验证提供了BNF语法[9-10]，具体语法含义如表1所示。

3.2 CTCS-3转CTCS-2的UPPAAL模型

根据前面所述对列车从CTCS-3级管辖范围驶入CTCS-2级管辖范围的过程分析，建立了列车跨越CTCS-3级区域向CTCS-2级分界点的等级转换的时间自动机网络模型TA=TATrain||TARBC||TADriver||TALTA||TALTO。列车跨越CTCS-3级区域向CTCS-2级分界点等级转换的时间自动机网络模型由Train子模型，RBC子模型，Driver子模型，LTA子模型，LTO子模型组成，分别如图3（a）～（e）所示。模型中a！表示某个子系统发送端发送消息事件a，a？表示某个子系统接收端接收消息事件a，以保证子模型中相同的转换同时发生。

4 模型的仿真与验证

在UPPAAL模拟器中对列车跨越CTCS-3级区域向CTCS-2级区域进行等级转换过程中出现的列车通过预告应答器LTA过程、收到转换预告命令后激活C2控制单元进行实际速度与C2允许速度比较的过程、请求司机进行转换确认的过程，到达转换执行应答器LTO执行转换的过程，列车尾部越过分界点后与RBC断开连接结束通信会晤的过程进行多次模拟。按照CTCS系统中，列车跨越CTCS-3级区域向CTCS-2级区域进行等级转换时，根据CTCS各子系统的性能和功能要求，对所建立的列车跨越CTCS-3级区域向CTCS-2级区域进行等级转换的时间自动机网络模型进行验证。用BNF语言描述的系统性能和功能要求如下：

（1）系统无死锁：A[]not deadlock，通过。

（2）列车能完成激活C2控制单元，越过转换分界点后转换为CTCS-2级控车以及尾部越过分界点后断开与RBC连接的功能：E<>（（Train.T_C2UnitActive）or（Train.T_C2-Control）or（Train.T_UnConnect）），验证通过。

（3）当司机在列车运行距离转换边界前5 s内未进行等级转换确认时，司机可在列车越过转换分界点转为CTCS-2级系统工作后5 s内继续进行确认：A<>（（Train.T_WaitConf1）imply（Train.T_C2 Control）and（T1>=5 and T2<5）），验证通过。

（4）车载控制器激活C2控制单元后会对运行速度进行监督，只有当运行速度低于C2允许速度时，才能实施等级转换由CTCS-3级转为CTCS-2級：E[]（（Train.T_C2UnitActive）imply（Train.T_C2-Control）and（NowSpeed<=250）），验证通过。

（5）转换预告点LTA距C3与C2转换边界的距离>10 s（车载与RBC通信时间5 s加司机确认时间5 s）：A<>（（Train.T_A-rriveLTA）imply（Train.T_1ArriveLTO）and（T3>10）），验证通过。

5 结语

本文采用时间自动机理论，以列车跨越CTCS-3级区域向CTCS-2级区域进行等级转换时CTCS-3级列控系统各个子系统之间的信息交互为依据，建立了列车跨越CTCS-3级区域向CTCS-2级区域运行时的时间自动机网络模型，并对所建立的模型进行了多次模拟仿真和修正。最后对列车由CTCS-3级转换为CTCS-2级所需的功能和性能要求进行了验证。验证结果表明：列车跨越CTCS-3级区域向CTCS-2级区域进行等级转换时，等级转换功能的完备性和正确性，保证了列车跨越C3/C2分界点时系统的安全性和受限活性。因此，此种方法适用于复杂系统需求规范的验证。

参考文献：

[1]董 昱.区间信号与列车运行控制系统[M].北京：中国标准出版社，2008.

[2]陈永刚，丁春平.基于TRSL的RBC等级转换场景研究[J].铁道标准设计，2016，60（8）：122-129.

[3]唐 涛，郜春海，黄友能，等.CJ/T407-2012城市轨道交通基于通信的列车自动控制系统技术要求[M].北京：中国标准出版社，2012.

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

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

[6]张紫菡，刘中田，王颖卓，等.基于UML语言的CTCS-1级车载ATP功能建模分析[J].铁路计算机应用.2017，26（5）：5-10.

[7]张曙光.CTCS-3级列控系统总体技术方案[M].北京：中国标准出版社，2008.

[8]丁春平.基于域+Timed RAISE的列控系统等级转换场景建模与验证[D].兰州：兰州交通大学，2016.

[9]王永伟.基于构件的形式化方法在软件开发中的应用研究[D].哈尔滨：哈尔滨工程大学，2010.

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