基于时间自动机的自主化ATP等级转换功能建模与验证

叶安君

(中铁第一勘察设计院集团有限公司，710043，西安//高级工程师)

我国现运营的高速铁路采用的是国产化CTCS-3级列车运行控制系统(以下简称“列控系统”)。中国铁路总公司是2014年开始开展自主化CTCS-3级列控系统技术研究的，研发了一批具有自主知识产权的自主化C3等级列控系统安全关键设备[1-2]。其中，自主化ATP(列车自动保护)系统是我国铁路的重要技术装备，是保证高速列车行车安全、提高运输效率的关键设备[3-4]。

自主化ATP系统在国产化ATP系统的基础上，增加和优化了一些安全功能需求，具有SIL4级的安全需求，一旦失效可能导致列车出轨等行车事故。目前，自主化ATP系统的研究主要集中在需求规范和系统测试方面[5-6]，理论研究相对较少。

时间自动机[7]具有严谨的数学基础，能够分析实时系统的功能逻辑需求及时间性能，在铁路信号安全关键系统中得到了广泛应用[8-9]。文献[10]采用时间自动机对ATP系统的超速防护功能进行形式化建模，验证了ATP系统的安全性和活性；文献[11]采用时间自动机分析了ATP系统的2乘2取2结构，验证了冗余结构的安全属性；文献[12-13]基于时间自动机分析了C3等级列控系统等级转换的系统需求；文献[14]基于时间自动机建立了等级转换时间自动机网络模型，验证了等级转换过程中的安全性和实时性；文献[15]采用时间自动机分析了自主化C3列控系统码序校验以及RBC(无线闭塞中心)切换等场景。研究表明，采用时间自动机对铁路信号系统进行建模和验证，对系统的需求分析和设计具有良好的指导作用。本文采用时间自动机方法，以自主化ATP系统的C2等级转换到C3等级功能为例，从理论上分析ATP系统需求的安全性、正确性和实时性，对自主化ATP系统的研究具有一定的理论意义。

1 自主化C3列控系统概述

1. 1 自主化C3列控系统发展过程

2007年，原铁道部成立C3技术攻关组开展C3列控系统的研发工作,在引进国外技术的基础上，实现了ATP和RBC设备的国产化，并成功应用于武广、郑西和京沪等高速铁路，这项研究对我国列控系统的发展和铁路装备现代化发挥了重要作用。

2014年，中国铁路总公司依托科研开发重点课题“列控系统设备自主化及技术要求研究”，开发具有自主知识产权的列控系统关键设备。2015年中国铁道科学研究院集团有限公司立项“CTCS-3级列控系统关键设备自主化研究”，专项对C3列控系统自主化研究进行重点研究。在中国铁路总公司的组织下，2016年6月至2017年1月，依托大西线综合试验段，对自主化C3列控系统进行了现场试验。2018年6—10月，以京沈高铁辽宁段为试验平台对自主化C3列控设备进行了综合试验，动态检测了自主化C3列控设备的功能及性能[17]。

1. 2 自主化C3列控系统的特点

自主化C3列控系统在国产化C3列控系统的基础上，对硬件、软件和功能需求都提出了新的要求。

1) 硬件、软件方面：自主化C3列控系统设备采用并列系工作，在保障系统安全性的同时增加设备可用性，拥有完全自主的知识产权。

2) 功能方面：自主化C3列控系统设备在国产化C3列控系统设备的基础上，增加了一些新的功能需求。以自主化ATP系统为例，新增加的功能需求包括：①C3行车许可融合轨道电路信息。C3主控单元计算轨道电路信息许可，并根据列车当前位置确定轨道电路信息许可终点。②在应答器报文中增加开门侧提示。③等级转换时，不需要司机进行确认。④使用JRU(司法记录单元)给各个主要模块进行校验时，保证各模块的系统时间保持同步。

2 自主化ATP系统等级转换功能

按照功能要求和设备配置划分，我国列控统划分为C0—C4共5个应用等级。同条线路上可以有多种应用等级，以满足不同线路速度的需求。自主化列控系统等级转换即是C3等级和C2等级之间的转换。

2. 1 C2等级向C3等级转换场景分析

自主化ATP系统等级转换功能包括C2等级向C3等级转换和C3等级向C2等级转换两种场景。这属于自主化ATP系统运行过程中重要的安全功能。列车如果未在指定的位置或时机转换到正确的运行等级，轻则可能造成行车中断影响行车效率，重则可能导致行车事故造成人员伤亡。从理论上分析和验证等级转换功能逻辑的安全性和准确性，对保证列车行车安全具有重要意义。

自主化ATP系统在C3等级控车时，系统接收轨道电路的编码信息，并与RBC发送的MA(移动授权)进行对比，判断是否一致。自主化ATP系统与RBC、轨道电路和应答器信息交互关系如图1所示。

图1 自主化ATP系统信息交互关系

本文以C2等级向C3等级转换为例进行分析。C2等级向C3等级转换典型运营场景包括：

1) 列车由C2等级运营线路进入C3等级运营线路，如列车驶出C2等级的动车段进入C3等级的运营线路。

2) 列车由于无线通信中断等原因由C3等级降级到C2等级后，需要重新转换到C3等级控车。

为保障等级转换功能的顺利进行，运营线路在地面设置了RBC连接点(RE)、等级转换预告(LTA)和等级转换执行点(LTO)3个转换点。当列车前端通过RE时，ATP根据应答器信息呼叫RBC并进行注册。当列车前端通过LTA点时，ATP将向RBC报告所在位置，RBC向ATP提供行车许可及等级转换命令。当列车前端通过LTO点时，ATP执行控车转换。

2. 2 C2等级向C3等级转换功能分析

C2等级向C3等级转换的过程主要包括列车与GSM-R网建立连接、与RBC建立通信会话、获取C3等级区域的MA和执行等级转换4个阶段，转换逻辑如图2所示。

图2 C2等级向C3等级转换序列图

1) 与GSM-R网建立连接。列车从C2等级向C3等级转换，首先要建立与GSM-R电台的连接。当ATP无线电台检测到GSM-R网后，自动与GSM-R网络建立连接。

2) 与RBC建立通信会话。与GSM-R网连接成功后，ATP呼叫RBC，向RBC发送列车位置报告。RBC向车载设备发送位置报告参数信息和MA请求参数信息。车载设备收到配置参数后向RBC发送确认信息。

3) 获取MA。列车前端通过预告应答器LTA后，RBC向车载设备发送包含C3等级区域的MA和等级转换命令。若ATP不能收到MA和等级转换命令，列车保持C2等级继续运行。当列车重新获得MA后，进行等级转换处理。在C3等级完全模式下，自主化ATP系统接收轨道电路信息的行车许可，因此，自主化ATP系统需要判断C2级行车许可和RBC发送的MA是否均越过等级转换边界。

根据自主化ATP系统C2等级向C3等级转换的功能，正常转换过程涉及应答器、RBC、C2行车许可、C3 MA等对象，转换过程中可能出现应答器丢失、无线通信中断、行车许可不一致(MA越过转换边界，但C2行车许可未越过)等故障场景。

3 时间自动机

时间自动机[18](TA)是针对带有时间因素的状态转换关系，在传统的有限状态自动机的基础上引入时间约束，提出的一种基于严谨的数学理论的描述方法，在实时系统的规范说明和形式化分析中占据重要地位。

定义1：时间约束

对于一个时钟变量集合X，时间约束δ的集合Φ(X)定义如下：

δ：=x≤c|c≤x|δ|┐δ1∧δ2，

其中，x∈X,c∈Q，δ1、δ2表示时钟约束。

定义2:时间自动机

一个时间自动机TA是一个六元组{S,S0,Σ,X,I,E}，其中：

S是一个有限位置的位置集合；

补救措施：一旦出现塌孔现象，需马上增加护筒长度并用机械压入。在下压过程中如遇硬物阻挡无法下压则应当适当加大或者缩小孔径，使护筒顺利下压，但两种方案都需重新处理护筒外的空隙。

S0是一个初始位置的位置集合，且S0⊆S；

Σ是一个有限字符的字符集合；

X是一个有限时钟的时钟集合；

I是一个映射，将S中的每个位置映射到Φ(X)中的某个时间约束；

E⊆SΣ2xΦ(X)S是转移的集合。

一个状态转移{s,a,λ,δ,s′}表示当系统输入字符a并满足时钟约束δ时，位置s迁移到位置s′。λ表示状态转移时，所有重置的时钟变量的集合。

UPPAAL软件是由瑞典Uppsala大学和丹麦Aalborg大学联合开发的时间自动机集成工具环境。UPPAAL软件对经典的时间自动机进行了扩展，包括编辑器、模拟器和验证器，支持时间自动机的建模、仿真和验证。UPPAAL软件采用on-the-fly技术，对时间自动机的可达性进行分析，进而能够验证系统的安全性和活性等系统属性。

4 C2等级向C3等级转换建模

根据C2等级向C3等级的转换逻辑，考虑到转换过程的复杂性以及转换过程中设备可能的故障，自主化ATP系统主要从正常转换和故障场景两个方面进行建模，如图3所示。对于应答器丢失故障采用故障注入的方式，将应答器丢失行为注入到正常转换模型中；对于无线通信中断和行车许可不一致故障单独建立时间自动机模型。

图3 自主化ATP系统时间自动机建模方法

C2等级向C3等级转换的时间自动机模型C2toC3TA划分为ATP时间自动机模型ATPTA、RBC时间自动机模型RBCTA、Balise时间自动机模型BaliseTA、通信状态时间自动机ConnectTA和行车许可时间自动机模型MATA5个部分，则C2等级向C3等级转换的时间自动机模型为以上5个时间自动机模型的积，即：

C2toC3TA=

ATPTA‖RBCTA‖BaliseTA‖MATA‖ConnectTA。

C2等级向C3等级转换的时间自动机模型如图4所示，模型中主要状态、变量的含义如表2所示。其中，ATPTA模型中注入了应答器丢失的场景，ConnectTA描述了无线通信中断的故障情况，MATA描述了MA越过等级转换边界，但C2级行车许可未越过的故障情况。

C2等级向C3等级转换的时间自动机模型具有1个时钟变量x，所有通道信号均为broadcast chan类型，所有变量均为int类型。以“?”结尾的标记表示接收到该信号时转换发生，以“!”结尾的标记表示发射该信号时转换发生。

1) ATPTA模型。主要描述ATP和RBC之间的交互信息，主要包括请求与RBC建立通信会话、发送列车数据、请求MA和执行等级转换等过程。当等级转换所有条件满足时，ATPTA转移到Switch状态，表示等级转换成功，ATPTA向RBCTA发送确认信息。ATPTA根据ConnectTA中Connect的值判断连接状态，连接失败时，转入SwitchFail状态，放弃等级转换。列车通过LTO时，ATPTA根据MATA中OverLTO的值判断是否存在制动，如果存在制动状态，ATPTA不进行等级转换。

2) RBCTA模型。主要描述RBC和ATP之间的交互信息，包括ATP与RBC建立连接、发送MA和发送等级转换命令3个部分。RBCTA根据ConnectTA的连接状态，判断ATP是否与RBC建立连接。在RBC与ATP成功建立连接的情况下，RBCTA与ATPTA交互列车数据、行车参数等数据，RBCTA根据列车位置及运行状态，向ATPTA发送等级转换命令。当列车通过LTO，但未接收到执行应答器信息时，即PassLTOState为2，ATPTA发送等级转换信号Switch。

3) MATA模型。描述C2级行车许可、C3级MA和等级转换边界的关系。当C2级行车许可和C3级MA均越过等级转换边界时，MATA将OverLTO变量置为1；当C2级行车许可未越过等级转换边界时，OverLTO为2。ATPTA根据OverLTO的值判断是否进行等级转换。

4) ConnectTA模型。描述列车与RBC的连接状态。当列车于RBC断开连接时，ConnectTA将连接状态Connect变量置为0，表示ATP与RBC连接失败。

5) BaliseTA模型。描述列车通过RE、LTA和LTO时的行为。当列车依次通过RE、LTA和LTO时，BaliseTA分别广播RE、LTA和LTO信号，ATPTA接收到RE信号后发送login信号，请求RBC注册。

5 C2等级向C3等级转换形式化验证

为验证C2等级向C3等级转换的时间自动机模型是否满足自主化ATP系统的需求，本文从安全性、活性和实时性3个方面，利用UPPAAL软件提供的模型检测技术对C2toC3TA模型进行形式化验证。

UPPAAL形式化验证的基本原理是用时间自动机M描述系统行为，用BNF语法描述系统属性φ，分析M是否为φ的一个模型M|=φ?。

UPPAAL软件提供的BNF语法如下：

图4 自主化ATP C2等级转换C3等级时间自动机模型截图

序号状态含义序号变量或信号含义1getPara获取行车参数7login请求注册RBC2Switch等级转换过程中8Connect通信状态,0表示中断,1表示正常3OverC2行车许可和MA均越过等级转换边界9switchCfm通知RBC等级转换成功4BeforeC2行车许可未越过等级转换边界10reset转换结束5PassLTORBC检测列车通过LTO应答器组11LTO列车通过LTO应答器组6LTOLostLTO应答器组丢失12PassLTOState列车通过LTO应答器组时的状态,1表示正常通过,2表示LTO应答器组丢失

φ::=E<>p|A[]p|E[]p|A<>p|p→q，

其中：E<>p表示p在1个状态转移序列s0→s1→…→sn的某个状态下为真，则E<>p为真，s0表示初始状态；A[]pnotE<> notp；E[]p表示存在某个状态转移序列s0→s1→…→sn，p在这个序列中的所有状态下都为真，则E[]p为真；A<>pnotE[]notp；p→q表示p为真则q为真。

根据自主化ATP系统需求，提取C2等级向C3等级转换过程中的安全性、活性和实时性要求。安全性指描述系统不期望发生的性质，如“连接RBC失败时，ATP能转换到C3等级”，通常表示“坏的事情不会发生”。活性描述了系统必定发生的性质，如“ATP能够由C2等级转换到C3等级”，通常表示“好的事情会发生”。实时性主要描述自主化ATP系统中的时间约束，如根据自主化ATP与RBC之间的通信功能，ATP与RBC连接超过10 s，则通信超时。自主化ATP系统形式化验证需求提取方法如图5所示。

自主化ATP系统C2等级转换到C3等级需要满足安全性需求：连接RBC失败时，ATP不能转换到C3等级，即ATP系统C2等级控车；未与RBC成功建立连接时，在任何情况下都不能转移到C3等级。根据C2toC3TA模型，该安全性需求的BNF描述如下：

图5 自主化ATP系统形式化验证需求提取方法

A[] ConnectTA.ConnectFail imply not ATPTA. SwtichSucc

采用UPPAAL软件的验证器进行形式化验证，验证消耗时间0.001 s，消耗内存6 884 KB。验证结果通过，表明C2toC3TA模型满足该安全性需求。

C2toC3TA模型的安全性、活性和实时性需要及验证结果如表3所示。验证结果表明，自主化ATP系统C2等级转换C3等级的系统需求满足指定的安全性、活性和实时性要求。

表2 自主化ATP系统形式化验证内容和验证结果

6 结论

本文针对自主化ATP系统的安全性、活性和实时性，采用时间自动机作为形式化建模和验证方法，以C2等级转换C3等级的安全关键功能为例，建立了自主化ATP系统C2等级转换C3等级的时间自动机模型；从安全性、活性和实时性3个方面，对时间自动机模型进行了形式化验证；从理论上分析了自主化ATP系统C2等级转换C3等级的功能逻辑。结果表明，自主化ATP系统满足期望的系统性质，基于时间自动机的形式化建模和验证方法对自主化ATP的系统需求分析具有一定的指导和应用价值。