车地协同列控系统追踪运行模块HCPN 建模与验证

2023-11-13彭永成李茂青岳丽丽

兰州交通大学学报 2023年5期

彭永成，李茂青，岳丽丽，王阳

（1.兰州交通大学自动化与电气工程学院，兰州 730070；2.中国国家铁路集团有限公司铁路安全研究中心，北京 100081）

目前，我国铁路运输处于快速发展阶段，列车运行控制系统作为轨道交通中的关键技术之一，为列车的安全、高效运行提供了保障。随着运营里程的增加和运行速度的提高，我国干线铁路列控系统实现了从CTCS-0（Chinese train control system level 0）到CTCS-3（Chinese train control system level 3）等级的国产化发展。然而，在城际铁路中，列控系统仍存在一些问题，主要包括：1）由于轨旁设备过多，导致系统造价昂贵；2）区间和车站采用不同控制系统，使得设备结构复杂，系统接口繁多；3）以地面为中心的控制模式使得信息流通环节较多，增加了通信延时。随着列车定位技术和适用于轨道交通的通信技术日益成熟［1］，为实现线路资源的充分利用和运营效率的进一步提升，有必要对下一代列控系统进行研究。文献［2］指出：我国列控系统应利用新技术简化和优化系统结构，结合无线通信、卫星定位和智能驾驶等技术进一步提高铁路运输效率，实现以车载设备为主体的列控系统架构。国内卡斯柯［3］和中车青岛四方［4］等单位也在进行下一代列车自主运行系统的相关研究，主要目的是实现轨旁设备的精简、系统功能分配的优化、以车载为中心的自主资源管理以及列车间隔的主动防护。文献［5］介绍了新一代列控系统的关键技术：以列车为中心的资源管理、列车自主控制和精简后的新架构，并对其优势进行了分析说明。文献［6］针对新型列控系统提出了线路资源管理子系统的概念，并设计了子系统的模块结构和线路资源管理流程。文献［7］提出了新型列控系统中邻域协作的管理模式和方法，并针对故障场景设计了基于邻域信息共享和控制模式切换相结合的列车群安全防护方法，以提高列车群整体对外界突发情况的应对能力。文献［8］设计了基于LTE技术的下一代CBTC数据通信系统，并对系统性能进行了测试，将性能数据转换为确定性随机Petri网模型参数，用于评估重连接和切换场景下系统的可靠性。文献［9］提出了适用于城际铁路的车地协同列控系统，无资源竞争时由车载设备实现进路功能，当多车竞争道岔资源时由地面目标控制器（object controller，OC）对车载或中心控制层的命令进行冲突判别与仲裁，完成对资源的分配。该系统在提升列车自主化的同时，继承了地面集中联锁进路控制的整体性及复杂车况的适应性。综合以上文献，由于新型列控系统处于开发试验阶段，尚无确定的系统方案及相关的技术标准，现有文献对车地协同列控系统追踪运行模块的研究较少，故需要对车地协同进行进一步研究。

新型列控系统作为安全苛求系统，其设计开发需完成功能安全性的测试和验证。若系统软件存在漏洞且产生不确定性行为，则有可能因影响正常运行而造成经济损失，甚至造成事故。对于系统功能的正确性和安全性问题，除了依靠传统的测试方法，在设计阶段，国际标准EN 50129－2018强烈建议使用基于严密的数学理论和推理的形式化方法对系统进行验证分析［10］。对于列控系统规范的建模与形式化验证，需要从系统规范到建模、验证之间建立完整的转换规则，保证系统规范、模型以及程序代码的高度一致性［11］，以消除自然语言可能造成的歧义。有色Petri网（colored Petri net，CPN）通过对系统结构和状态变化的精确描述，分析复杂系统运行过程中的并发性、异步性和不确定性行为，以检验系统状态是否有不符合要求的异常标识［12］。近年来，有色Petri网已经成为列控系统建模和验证的一种重要理论方法。文献［13］利用有色Petri网对无线闭塞中心（radio block center，RBC）进行建模，研究了列车通过RBC 边界时进行RBC 切换的问题，并分析了影响切换的原因和提高成功概率的方法。文献［14］利用有色Petri网对列车运行过程中不同等级列控系统之间的转换建立形式化模型，分析了列车速度和等级转换实时性之间的关系。文献［15］对铁路平交道口控制系统建立了适用于定量安全分析的系统定时分层CPN 模型，通过探索标准的状态空间报告来验证非时序CPN 模型，并基于模型仿真过程中采集的数据评估危险事件平均时间的安全特性。文献［16］利用有色Petri网理论，研究了不同的后备模式下设计间隔对列车模式切换成功率和运行效率的影响，得到了列车模式切换的成功率和后备模式设计间隔的关系。文献［17］针对基于卫星定位的列控系统，在不同场景下对车载子系统构建有色Petri网模型，并将所有场景整合成一个连贯的整体模型，采用状态空间分析和基于模型的测试技术验证CPN 模型在标准和系统特定属性方面的正确性和一致性。对列控系统的建模验证时，将系统划分为不同的功能子模块，以便于分析系统的具体功能。另外，通过接口库所将不同场景下建立的子模型连接，构成系统顶层模型，以保证验证分析时模型与系统设计的一致性。

本文基于文献［6］中适用于城际铁路的车地协同列控系统，进一步研究其追踪运行模块的实现。首先，基于车地协同系统的架构和特点，对列车追踪运行的功能实现做合理设计，其移动授权计算由车载设备实现，从而优化功能分配，提高列车自主化程度；其次，采用分层有色Petri网（hierarchical coloured Petri net，HCPN）对移动授权生成和安全防护功能的具体实现过程建立层次化模型，描述系统运行中的信息交互和状态变化；最后，基于具体的数据，利用模型检验方法对模型状态空间及节点状态进行分析，为列控系统的具体开发提供理论支撑。

1 车地协同系统追踪运行模块功能实现

1.1 车地协同列控系统整体结构

车地协同列控系统的结构分为地面站内设备、车载设备和地面轨旁设备3个部分，通过通信网络实现信息交互。各部分子模块之间传递的信息如图1所示。

图1 列控系统子模块间传递的信息Fig.1 Information transmitted between sub-modules of the train control system

地面中心的调度集中系统（centralized traffic control，CTC）承担与调度运营相关的业务，行调人员通过CTC系统将行车计划和临时限速命令下发到列控系统。在车站内设置地面列车管理单元（train management unit_center，TMU_C），接收CTC发送的信息，并将其作为管辖范围内列车运行和进行作业的依据。TMU_C将收到的运行计划和临时限速命令进行解析，发送给对应列车的车载设备；同时，TMU_C会收集管辖范围内列车的实时运行状态，并转发到该范围内列车车载设备。此外，在TMU_C中设置电子地图数据库，描述最新线路固定信息，包括用于辅助定位和进路触发等功能的虚拟应答器、线路资源类型和线路固定限速等信息。当有列车进入TMU_C管辖范围时，会通过TMU_C对车载电子地图版本进行校核和更新。

地面轨旁设备取消了信号机、轨道电路，站内增设目标控制器（OC）与线路道岔资源一一对应，用于实现对道岔的征用以及对车载或中心控制层的命令进行冲突判别与仲裁。

车载设备主要包括追踪运行模块、联锁模块、车载列车管理单元（train management unit_vehicle，TMU_V）和其他辅助模块。联锁模块实现列车进路控制，向OC申请占用道岔资源，从而完成进路的建立和解锁等功能。追踪运行模块由车载移动授权计算单元（movement authority unit，MAU）、超速防护模块（automatic train protection，ATP）和自动驾驶子系统（automatic train operation，ATO）构成。追踪运行模块实现列车的运行控制，保证列车在允许的范围内以合理速度运行，且在追踪运行时主动和前车保持间隔。

车地协同列控系统改变了现有列控系统以地面中心设备为主体的系统架构，由车载和地面设备协同完成列车进路管理和追踪运行控制功能，这有利于实现多车对道岔抢占与共享场景下的联锁功能，避免列车间的进路冲突。

1.2 追踪运行模块功能实现

追踪运行模块的功能可划分为移动授权生成、超速防护和自动驾驶。追踪运行模块从其他模块获得的信息包括：

1）从电子地图模块获取线路静态数据；

2）与车载列车管理单元（TMU_V）实现信息交互，获取相邻列车实时位置和其他静态障碍物（如站台门、紧急停车按钮等）信息；

3）与车载联锁模块通信，实现对进路信息的实时更新，并将其作为车载设备计算进路移动授权（movement authority，MA）的条件。

1.2.1 移动授权计算单元功能实现

车地协同列控系统中，移动授权的生成由追踪运行模块中的车载移动授权计算单元（MAU）实现。MAU 根据来自前方相邻列车和地面设备的线路障碍物信息，确定列车运行前方最近的障碍物，并将其设为移动授权终点（end of authority，EOA）。从本车车尾到该EOA 范围内线路，按照允许的运行方向被授予列车使用，作为控制列车运行的依据。

车载移动授权计算单元在自主计算移动授权时，与其他子模块的信息交互如图2所示。中心设备获取管辖范围内各列车信息，并转发给车载TMU_V。车载联锁子系统收到行车计划后，请求线路资源并向OC 发送操作命令。MAU 模块周期性地更新运行前方线路的静态障碍物信息、前方列车信息和由联锁子系统处理生成的进路信息，并结合电子地图自主判断最近障碍物及其类型，得到移动授权终点。MA 计算完成后，MAU 模块将该信息输出至超速防护模块。

图2 MA计算阶段各模块信息交互图Fig.2 Information interaction in the MA calculation phase

MA 计算流程如图3所示。列车运行时，车载自主定位单元实时获取列车所在位置，根据运行情况和自身参数信息，计算考虑了安全包络的位置信息。若路径探询范围内有前车，则需根据前车的位置、速度、测距误差、通信延时等信息计算出前车可能存在的位置，并在计算时考虑列车移动距离，从而对列车追踪间隔进行优化。

图3 MA计算流程图Fig.3 Flow chart of calculation for MA

在MA 计算阶段，首先，MAU 依据TMU_V转发的线路静态障碍物信息，判断运行前方是否探询到无权限的线路资源，包括由设备故障或者特殊情况导致的状态异常资源。然后，MAU 根据电子地图确定列车是否处于进路触发位置，再进一步判断前方是否有进路或者列车，从而确定列车所处的场景是追踪前车运行还是触发进路，以及是否处于线路端点或者折返点。在此过程中，对于EOA 的计算与当前所处的场景相关，通过获取到的障碍物信息确定其类型及具体位置。若得到的EOA 要求列车立即停车或到此EOA 的距离不满足安全制动距离，则需根据场景判断是否向车载发送紧急制动信息；若该EOA 无需输出紧急制动，则确定MA 的范围。MA 起点为本列车安全车尾，从该位置开始到EOA，遍历线路区段、道岔等线路资源状态，串接可用线路资源，从而实现MA 的延伸。在授权终点前预留一定的安全距离，以确保列车在静态障碍物前安全停车，或在对前方列车追踪运行过程中与前车保持安全间隔。根据判断出的不同场景，对于MA 范围内的线路资源做不同的处理。最后，根据电子地图，在已确定的MA 线路中加入固定限速值。在计算MA 时，由列车当前的运行情况决定需要向前探询的范围，以减少对线路资源的不必要占用，从而实现对地面线路资源的优化利用［18］。

1.2.2 超速防护模块功能实现

超速防护模块（ATP）中的信息处理流程如图4所示。其功能主要由以下3个阶段实现：

图4 超速防护模块信息处理Fig.4 Information processing of overspeed protection

1）ATP在获取由MAU 自主计算生成的移动授权后，与TMU_V 通信，检查是否收到CTC 下达的临时限速命令，若已下达则需添加该命令。

2）更新当前位置信息，根据列车最大制动距离生成速度监控曲线，发送给自动驾驶子系统（ATO），由ATO 完成对速度监控曲线的跟踪。

3）在列车运行过程中，ATP 根据列车当前的位置和实时速度信息，与速度监控曲线进行比较，判断是否达到制动条件，若触发制动，则立刻输出相应等级的制动命令。ATP严格监控列车的速度，根据需要生成警告信息，确保列车不越过移动授权终点。若当前时刻已输出紧急制动，则在列车停车之前持续输出紧急制动命令。

2 追踪运行模块建模

有色Petri网对大型复杂系统的并发性、异步性的精确描述和直观的图形表达能力，常被应用于铁路信号软件的形式化建模与验证中。在CPN 中，用库所（place）表示一个或多个状态量，用变迁（transition）描述状态量的变化，模拟系统行为，用有向弧（arc）连接库所和变迁，弧上的函数描述状态的变化。通过标准元语言（standard meta language，SML）实现模型中函数的编译。SML语言常被用于编译器、编程语言研究以及自动定理的证明研究。在CPN 模型中，SML 语言能够自动地指定多数表达式的类型，不要求显式的类型标注，而且能够确保类型安全，有良好类型的SML 程序已被证明不会导致运行时间类型的错误［19］。

2.1 追踪运行模块顶层模型

本文采用自上而下的建模思路建立分层CPN模型，以降低模型的复杂度。将功能实现过程进行划分，不同功能由替代变迁代表的不同子模块完成。对于邻车和其他功能作简化抽象处理，主要对追踪运行功能建立精细化模型并对此功能的实现和安全性进行验证。

在CPN模型中，用颜色集表示数据类型，部分颜色集定义如图5所示，其中：TRAINID颜色集表示列车号，DIR颜色集表示列车的运行方向，LINEPOS表示线路位置。由标准颜色集可以构造出其他类型颜色集，TRINF是一个乘积类型（product）颜色集，由列车号、车头位置、车尾位置以及运行方向复合而来，表示列车位置信息。为便于描述，将线路的属性分为站内无岔、站内有岔、区间和尽头型，用颜色集MAPINF描述电子地图中线路信息。SWITCH 颜色集表示道岔信息，包括道岔编号、道岔位置以及经过该道岔时的限速。ROUTEINF表示经联锁子系统处理的可用进路信息，用来确定列车的初始位置、进路的始终端位置及进路内道岔的开通位置。移动授权计算完成后，其范围内每个虚拟区段的信息由颜色集合MASEC表示，最终以列表颜色集LISTMASEC类型输出。在超速防护子模型中，颜色集SMTYPE表示区段所处的监控区类型，SMSEC为被监控区段的信息，LISTSMSEC为SMSEC的列表形式。

图5 颜色集声明Fig.5 Declaration of color set

追踪运行模块顶层模型中设置5个代替变迁，分别完成追踪运行模块的不同功能，如图6所示。代替变迁Safe_position_process1 和Safe_position_process2对应于安全位置处理子模型，分别完成本车和邻车的安全位置计算，其结果由库所Train_safe_position和Nei_train_safe_position表示。代替变迁MAU_process对应于移动授权计算子模型，判断列车当前的场景并计算得到MA，然后输出到库所MA_list。代替变迁ATP_process和ATO_process分别对超速防护子模块和自动驾驶子模块建模。ATP_process子模型接收临时限速信息TSR_inf和列车当前动态信息Train_dyn_inf，输出制动命令到库所Brake_output；Monitoring_speed是一个接口库所，通过此库所可将ATP_process子模型生成的速度监控曲线传递给ATO_process子模型。

图6 追踪运行模块顶层模型Fig.6 Top model of the tracking operation module

2.2 MAU 模块模型

移动授权模块模型如图7所示。初始状态时，由进路信息Routeinf、邻车位置信息Nei_train_safe_position和无权限的线路资源Nonprivileged_resource触发代替变迁EOA_process。在EOA_process对应的子模型中，通过查询电子地图Map_e确定运行前方的唯一列车，从而对比障碍物位置得到当前EOA 信息。此外，为防止将非安全位置作为后一阶段计算条件，非安全列车位置Train_positoin和Nei_train_position的状态被设置为EOA_process触发的限制条件，若未得到安全位置，则不能开始EOA 计算。最后，根据不同的列车运行场景，结合EOA 类型选择不同的算法，分别由代替变迁MA-r_process和MA-o_process表示授权终点为进路终端和障碍物类型时的MA 计算。

图7 MAU 模块（MAU_process）模型Fig.7 Model of the MAU module（MAU_process）

当EOA 被判断为唯一前车时，建立的子模型如图8所示。该模型描述此场景下MA 计算的具体实现过程。根据CPN 消息驱动机制，若在库所Fro_train_safe_position上有托肯，则表示已经确定前方唯一列车为MA 终点障碍物；若库所Safe_position上有托肯，则表明前一阶段已计算出本车安全位置。

图8 EOA为前车尾部时的MA计算（MA_obstacle process）子模型Fig.8 Sub-model of the calculation for MA in the scene when EOA is the rear of front train

在此场景下，首先，确定MA 起点和终点位置，库所MA_startpoint表示MA 起点为本列车安全位置的尾部，库所MA_endpoint表示MA 终点为前车尾部安全位置；由于此模型中已判定该范围内线路资源空闲且可用，故可确定MA 范围内的线路区段。之后，变迁MA_end_generate和MA_start_generate结合库所Map_e中的电子地图信息，通过周围有向弧上的函数，将满足条件的线路资源进行串接，同时确定线路固定限速。最后，库所MA_sec_list将MA线路以列表形式输出，由端口库所MA_to_frt_train表示EOA被判定为前车尾部时的移动授权。

2.3 超速防护模块模型

超速防护模块模型如图9所示。初始状态时，库所MA_list表示经移动授权模块计算得到的MA信息。该模型主要分为3个部分：第1部分，由代替变迁TSR_process将临时限速命令TSR_inf添加到MA 范围内的区段信息中；第2 部分，由代替变迁Monitoring_speed_process根据列车本身参数得到控车曲线，并通过接口库所Monitoring_speed和Monitoring_speed_for_ATO 输出；第3部分，由代替变迁Dyn_protection 根据列车当前位置和动态信息（速度、加速度、制动情况）监控列车实时运行。以上3个代替变迁对应的子模型完成各自具体功能，最终实现列车运行时对速度的安全防护。

图9 超速防护模块（ATP_process）模型Fig.9 Model of the overspeed protection module

速度实时监控子模型（Dyn_protection模型）如图10所示。变迁Monitoring_speed输入速度监控曲线信息，同时产生托肯给库所Trigger1 和Trigger2，用于提供其他变迁的触发条件。更新列车位置信息后，变迁TSM_process和CSM_process通过守卫函数，分别完成在不同监控区对列车限速信息的处理。在列车动态信息输入阶段，由变迁EB_judge判断列车当前制动等级，若此时已输出紧急制动命令，则继续输出紧急制动；若未输出，则由变迁Braketype_judge1 和Braketype_judge2 及周围弧函数根据列车位置和当前速度输出对应等级的制动。最终的制动命令输出至端口库所Brake_output，表示超速防护模块与列车制动单元的接口。

图10 速度实时监控子模型Fig.10 Sub-model of the speed monitoring module

3 追踪运行模块功能验证

考虑多车在区间追踪运行的场景，通过建立的模型对追踪运行模块功能进行验证。设区间内有3辆列车追踪运行，前方列车分别为Train（1）和Train（2），本列车为Train（3）。改变输入库所的托肯值，以设置模型的初始状态。库所Train_positoin的托肯值设置为（Train（3），（19，2 800），（19，3 000），down），表示本车实时位置和运行方向；库所Nei_train_position的托肯值设置为1｀（Train（2），（21，6 000），（21，6 200），down）＋＋，1｀（Train（1），（23，7 900），（23，8 100），down），表示前方2辆列车位置信息；库所Nonprivileged_resource 的托肯值设置为（switch，（27，11 600），（27，11 700）），表示前方无权限资源的类型及位置；库所TRAIN_dyn_inf的托肯值设为（Train（3），260，nb，down），表示列车速度为260 km／h，未处于加速或制动阶段。将本场景下建立的模型逐步执行，可观测到模型的状态变化，利用模型分析工具可生成状态空间报告［20］。

3.1 移动授权生成功能验证

移动授权模型标准状态空间统计数据中，状态空间的可达状态节点数量为264个，托肯绑定弧的数量为533个，统计状态为完全；强连接组件图中，可达节点数量为264个，托肯绑定弧的数量为533个。

移动授权模型状态空间统计结果状态为完全，表明计算出的状态空间是完整的，模型的所有可达状态节点已被纳入统计，可达状态节点和托肯绑定弧的数量均为有限值，终节点标号为264。由于强连接组件图与状态空间中的状态节点数量和托肯绑定弧数量相同，故模型中不存在活锁。由图11中的模型家态性（Home Properties）和活性（Liveness Properties）报告可知：在此场景下，模型的家态节点（Home Markings）和唯一死节点（Dead Markings）的标号都为264，与终节点标号一致，表明系统总是可以到达最终节点；模型存在死变迁（Dead Transition Instances），由报告可知为移动授权模块收到多个静态障碍物信息或进路信息时对于障碍物的处理变迁，由于所选场景中静态障碍物是唯一的且没有进路信息，故该变迁不会触发，系统的活性满足场景要求；由模型公平性（Fairness Properties）报告中“No infinite occurrence sequences”可知，模型不存在无限发生的序列，不会循环执行，满足公平性要求［21］。

图11 移动授权模型状态空间报告Fig.11 State space report of the MAU model

对移动授权模型可达节点的状态及对应库所的具体托肯进行检查可知：无异常节点，模型功能安全性满足设计需求。由状态空间统计结果可知：统计模型终节点标号为264，顶层模型在该节点处库所的具体托肯值如图12所示。由图12可知：库所MA_list的托肯值为1｀［（Train（3），（19，2 780），（19，4 600），section，180），（Train（3），（21，4 600），（21，5 920），section，200）］，表示模型最终状态已计算出该场景下从本车到唯一前车的移动授权。

图12 移动授权模型终节点托肯值Fig.12 Token of the ultimate node in MAU model

由模型初始状态中列车当前位置和前方障碍物信息，可确定本车Train（3）在区间对前方列车进行追踪运行，且前车Train（2）被确定为前方唯一障碍物。从本车安全车尾位置到前车车尾的线路资源应为（19，2 780）、（21，4 600）、（21，5 920），与图12模型终节点中移动授权的线路资源一致。该线路区段的限速值分别为180、200 km／h，与电子地图中限速一致。

3.2 超速防护功能验证

超速防护模型标准状态空间统计数据中，状态空间的可达状态节点数量为237个，托肯绑定弧的数量为386个，统计状态为完全；强连接组件图中，可达节点数量为237个，托肯绑定弧的数量为386个。

超速防护模型状态空间统计结果状态为完全，表明计算出的状态空间是完整的，模型的所有可达状态节点已被纳入统计，可达状态节点和托肯绑定弧的数量均为有限值，终节点标号为237。由于强连接组件图与状态空间中的状态节点数量和托肯绑定弧数量相同，故模型中不存在活锁。家态性（Home Properties）和活性（Liveness Properties）报告见图13。模型的家态节点（Home Markings）和唯一死节点（Dead Markings）为同一节点，且标号与终节点一致，表明系统总是可以到达最终节点。模型的死变迁（Dead Transition Instances）为EB_judge。由于初始状态下未输出紧急制动，故此场景下不会触发该变迁，系统活性满足要求。由模型公平性（Fairness Properties）报告中“No infinite occurrence sequences”可知：模型不存在无限发生序列，不会循环执行。

图13 超速防护模型状态空间报告Fig.13 State space report of the overspeed protection module

对超速防护模型可达节点的状态及对应库所的具体托肯进行检查可知：无异常节点，模型功能安全性满足设计需求。模型的终节点中具体托肯值如图14 所示。库所Monitoring_speed的托肯值为1｀［（（2 780，4 600，19，180），tsm），（（4 600，4 800，21，200），tsm），（（4 800，5 800，21，180），tsm），（（5 800，5 920，21，200），tsm）］，以列表数据形式表示超速防护模块生成的监控速度。库所Brake_output的托肯值为1｀eb，表示成功输出紧急制动命令。

图14 超速防护模型终节点状态托肯值Fig.14 Token of the ultimate node in overspeed protection module

由于列车位置在初始状态时设置为［（19，2 800），（19，3 000）］，考虑列车安全包络后到前方障碍物的距离为2 600 m，当列车以0.8 m／s2为最大减速度进行制动情况下，在该位置可以安全停车的最大运行速度为246 km／h，而当前列车实时速度设置为260 km／h，故需输出紧急制动，与模型输出制动等级一致，满足系统功能安全性需求。