基于车车通信的列控系统移动授权功能建模与验证

陈 燕

（福州职业技术学院交通工程系，福建 福州 350000）

1 基于车车通信的移动授权功能

1.1 基于车车通信的列控系统

列控系统，即列车控制系统，是保证列车安全、高效、舒适运行的关键系统之一。基于车车通信的列控系统主要实现动车组与动车组之间的直接信息传输，包括速度、位置、列车识别等，正因为如此，列车可直接进行移动授权计算而无需轨旁设备计算后转发，避免了传统列控系统中需要通过轨旁设备实现信息传输的局限性，提高了信息传输的效率和可靠性[1]。车车通信列控系统还可以实现动车组之间的协同控制，提高列车的运行效率和安全性。同时，由于移动授权计算功能由车载设备完成，地面设备得到简化，系统复杂度和运维成本降低[2]。

1.2 移动授权生成功能

移动授权（Mobile Authority，MA）是列车运行的前提，它决定了列车的限速及终点信息。传统列控系统的移动授权计算由轨旁区域控制器ZC 来完成，一个ZC 管辖范围内可能存在多辆列车同时运行，一旦故障，将导致大量列车延误[3]。而基于车车通信的列控系统中移动授权的计算以车载移动授权模块为主，以智能列车监控系统、对象控制器等其他子系统为辅来完成计算[4]。移动授权的目标点可能是信号机、道岔等静态障碍物，也可能是前方运行车辆等动态障碍物，同时计算过程还需考虑线路条件以及临时限速信息，所以列车需要与地面设备通信获取这些静态障碍物、线路条件等信息，同时还要不断与前行列车进行通信获取动态障碍物信息。

2 形式化建模

2.1 形式化建模理论

形式化建模理论是一种数学建模方法，用于描述和模拟现实世界中的各种现象和过程。它基于数学符号系统，使用形式化语言来描述模型，并使用计算机程序来验证模型的正确性和可靠性。形式化建模理论的主要目的是提供一种精确、一致和可靠的方式来描述和模拟现实世界中的系统，协助排查系统中可能存在的漏洞，提升系统运行的稳定性。

形式化建模理论包括三个主要组成部分：模型、解释和验证。模型描述系统或过程的本质特征和行为。解释模型并回答模型所描述的问题。验证检查模型的正确性和可靠性。

列控系统是对于安全性能有着近乎苛刻的要求，车车通信的应用提升了车载设备的复杂度，原有模块在功能和信息交互上也有了变化，以前车车尾为终点的移动授权计算模式需要高频次的进行实时移动授权计算以保证列车运行效率和安全性能，针对基于车车通信列控系统的实时性、连续性的特点，选择有色Petri 网理论为基础，遵循分层建模的原则建立模型。

2.2 有色Petri 网理论

有色Petri 网理论在普通Petri 网的库所和变迁的基础上，引入了颜色（有色）的概念，用于描述和研究复杂系统的动态行为。库所的颜色表示系统的属性，变迁的颜色表示系统可以执行的操作。有色Petri网理论的优势在于它可以更准确地描述具有多个属性的系统，包括系统的演化、系统的稳定性、系统的控制等问题。

CPN Tools 工具是针对Petri 进行模型设计、功能验证的工具，可实现模型的可视化，提供系统的可达性、有界性、活性、回归性和公平性的状态空间分析报告，发现模型中的漏洞，从而改进完善模型。

3 移动授权计算模型的验证分析

3.1 车载移动授权生成流程

列车运行前，先根据预先下载的电子地图规划运行路径，然后与对象控制器通信，遍历目标路径上的虚拟信号及道岔信息，若信号开放、道岔位置正确、路径范围无站台、并且已识别出唯一前车并建立通信，那么列车就以前车车尾为终点障碍物，否则就以不符条件的设备为终点障碍物[5]。接下来以本车车尾为起点，再结合线路的临时限速信息计算移动授权。在运行过程中还需不断与智能列车监控系统、对象控制器以及前车进行通信，获取线路条件、道岔位置、前车运行状态等信息，不断计算新的移动授权，保证列车运行在最优的状态[6]。

3.2 顶层模型建立

根据车载移动授权生成流程建立其顶层模型如图1 所示，该模型包含静态障碍物信息处理（Static）和动态障碍物信息处理（Dynamic）2 个变迁，包含车载移动授权模块（V_MA）、静态障碍物判断结果（Static_Result）、终点为静态障碍物的MA（S_MA）和终点为动态障碍物的MA（D_MA）共4 个库所，用STRING定义颜色集info。

图1 移动授权计算顶层模型图

3.3 子模型建立

根据终点障碍物类型可将模型分为静态障碍物处理模型和动态障碍物处理模型。

静态障碍物处理模型用来模拟列车运行路径终点为静态障碍物的情况，其处理模型如图2 所示，总共包括从对象控制器获取路径上的静态障碍物信息（Static）、判断路径上的虚拟信号状态（XH_State）、判断道岔状态（DC_State）等3 个变迁，包括开始计算移动授权（V_MA）、判断信号状态（XH_Judge）、信号判断结果（XH_Result）、判断道岔位置（DC_Positon）、判断道岔状态（DC_Judge）、静态障碍物判断结果（Static_Result）等6 个库所。

图2 静态障碍物处理模型

列车开始计算移动授权时，首先通过对象控制器遍历路径上的虚拟信号状态，并将结果存放在Signal中，如果信号未开放，那么列车就以虚拟信号位置为终点计算移动授权，如果信号开放，则继续遍历道岔状态，如果道岔位置正确，再根据前车位置计算移动授权，如果道岔位置不正确且无法转换，则以道岔位置为终点生成移动授权，最终将最新的移动授权存放在Static_Result 中。

动态障碍物处理模型用来模拟列车运行路径终点为唯一前行列车的情况，其处理模型如图3 所示，总共包括从对象控制器获取路径上的动态障碍物信息（Train_State）等2 个变迁，包括通过静态障碍物处理模型计算得到的静态障碍物判断结果（Static_Result）、根据静态障碍物生成的移动授权（S_MA）、继续进行其他信息的判定（Msg_Judge）、前车信息（V_Ahead）、移动授权计算结果（D_MA）等6 个库所。

图3 动态障碍物处理模型

如果规划路径上存在未开放的信号或者位置不正确且无法转换的道岔，则以S_MA 中存放的静态障碍物信息为终点生成移动授权，如果信号和道岔位置均满足条件，则以唯一前车位置为终点计算移动授权，如果不存在前车，则以列车运行目标为终点生成移动授权。

3.4 移动授权计算模型验证与分析

3.4.1 模型逻辑功能验证

根据图1 的移动授权计算模型图，库所VOMA为其初始状态，当托肯为1`（“MA”）时，列车开始计算进入移动授权计算流程。可能出现虚拟信号未开放、道岔位置不正确等情况，此时应以未开放信号或者错误位置道岔为终点计算静态移动授权（Dev_MA），列车在运行过程中可能存在没有前车的情况，此时应以列车运行目标位置为终点计算移动授权，进而由车载ATP 生成位置速度曲线控制列车安全运行。如表1 所示，功能正常与功能特殊情况都可实现。

表1 移动授权模块功能验证

3.4.2 模型状态空间分析

由图4（a）为移动授权生成模型部分状态空间报告，可以看到State Space 与Scc Graph 中的节点和弧的数量一致，系统所有节点可达。

图4 移动授权生成模型报告

图4（b）为移动授权生成模型系统有界性报告，可以看到模型中仅存在1 个Upper 和Lower 均为0的库所，这是因为该库所存放由静态障碍物生成的移动授权，模型中默认初始状态是虚拟信号机都开放，道岔位置正确且锁闭，因此出现这种情况，整个系统模型有界。

图4（c）为移动授权生成模型性质报告，可以看到 Dead Transition Instances、Live Transition Instances、Fairness Properties 都为None，表示没有重复的流程，满足公平性的要求。通知可以看到Dead markings 显示节点6 为死节点，因为节点6 是模型的最后一个节点，所以符合实际情况，模型具有活性。

4 结语

采用有色Petri 理论对基于车车通信的移动授权计算流程，根据分层建模的思想，建立了移动授权计算的Petri 模型，并完成了模型的空间、有界性及性质报告，得出了该模型满足可达性、有界性、公平性、活性的要求，该模型在基于车车通信的列控系统中合理且有效，实现系统功能并能满足系统的安全性需求。