基于形式化方法的城轨FAO系统在线危险预测技术

杨艳艳，王 祺，柴 铭，3

（1．北京城市轨道交通咨询有限公司，北京 100068；2．北京交通大学电子信息工程学院，北京 100044；3．轨道交通运行控制系统国家工程研究中心，北京 100044）

1 概述

近年来城市轨道交通取得了飞速发展。全自动运行（FAO）是进一步解决高速、高密度城市轨道交通安全、高效、节能、灵活运输的重要手段，是目前城市轨道交通的重要发展方向。

FAO系统是一种在基于通信的列车运行控制系统（CBTC）上将列车驾驶员/调度员执行的工作由自动化、智能化的设备所替代的控制系统。其优势主要表现为：通过减少人因影响提高系统的安全性和可靠性；提高系统运行效率及列车运行准点率和舒适度；降低系统整体能耗；降低系统全生命周期成本。

与CBTC系统相比，FAO系统更加智能，软件承担的安全功能及处理的异常场景更为复杂，系统组件间以及和人员、环境之间的交互更加复杂。此外，对于FAO系统而言，由于软件承担了更多的功能，减弱了司机在系统失效时的防护作用，给行车安全带来了新的挑战。

目前已有EN 50128和EN 50129等铁路控制与防护标准规范轨道交通系统不同安全级别(SIL0～SIL4)的软件设计与测试，尤其是对于高安全性功能（SIL3和SIL4）强制要求使用形式化方法保障安全性。但是，由于FAO系统涉及计算、通信与控制这3个方面的高频实时协作，其系统设计与实现异常复杂，传统的形式化验证方法存在状态空间爆炸问题。

为解决上述问题，本文基于一种运行时验证的形式化方法，通过构建形式化监控器实现对FAO系统运行时行为的实时验证，预测列车运行危险并施实报警，将系统导向安全侧。相比于传统的形式化验证，该方法可降低计算复杂度，为FAO系统的实验室完备验证提供有效手段，以保证系统安全。

2 FAO的运行时验证系统

2.1 运行时验证系统框架

运行时验证系统框架如图1所示。该系统与FAO系统并行运行，实时预测FAO系统的运行行为。运行时验证系统中包含列车控制模型，根据列车运行时行为计算模型中列车未来所有可能行为的可达集，进而通过判断可达集是否满足安全约束，实现对列车运行危险的预测。

图1 运行时验证系统框架Fig.1 Framework of runtime verification system

2.2 FAO系统运行控制模型

运行时验证系统的核心是参数化模型，该模型为参数化混成自动式，是列车运行控制行为的形式化描述。该模型如图2所示。

该模型包含4个状态，分别代表牵引（ACC）、惰行（COA）、常用制动（SB）和紧急制动（EB）。状态间通过列车的速度、位置关系实施状态迁移。上述关系通过状态迁移条件描述，当列车的速度位置满足迁移条件时，则发生状态迁移。由于紧急在停车前无法缓解，因而该状态只有迁入而无法迁出。列车的运行行为由状态中的流条件（Flow）描述，即ṡ=v,v˙ =a-w(s,v,a,w分别代表列车走行距离、速度、加速度和阻力)。

在实际应用中，不同线路中列车拥有不同的阻力，且不同移动授权条件下列车的迁移、制动速度位置关系亦有所不同，因而模型采用参数化建模方法，模型参数每周期根据车载运行时数据及相关线路工程数据配置，以得到符合列车实际运行状况的实例化模型进行验证。

模型的参数依据列车动力学模型计算：基于微分方程理论，通过如公式（1） 、（2）所示的列车受力特征及动力学定律模型，描述列车的速度位置约束关系，从而得到列车运行控制形式化模型中的参数取值。

其中，Se/km代表制动距离，b/（N/kN）代表单位制动力，w0/（N/kN）代表单位基本阻力，wr/（N/kN）代表单位坡度附加阻力，g为重力加速度（取9.8m/s2），M/t代表列车质量，v0/（km/h）代表列车初始速度，ve/（km/h）代表列车经过一段制动后的速度，φh代表闸瓦换算摩擦系数，→代表每个车轮施加的闸瓦力。

2.3 模型可达集计算算法

FAO系统形式化模型的可达集是指所有可能出现的列车速度位置状态的集合。对于一般的混成模型而言，其复杂度过高会导致模型无法在合理时间内计算其完备的执行轨迹，因而需进一步基于模型的过近似理论，利用多面体（Zonotope）精化模型可达集以提升列车行为预测效率。该方法的原理如图3所示。

图3 多面体模型可达集计算理论Fig.3 Theory of computation of reachable set for polyhedral model

该方法基于对任意中心状态的演化矢量，得到所有可能的下一状态。进而以下一状态为中心状态，计算新的演化矢量。该过程迭代进行，直至状态不再演化或满足预设的终止条件。

2.4 FAO系统安全约束

FAO系统的顶层危险为列车超速和越过移动授权终点（EoA）。该危险有多种致因，包括车载线路坡度计算错误、测速测距故障、地面进路办理错误、移动授权(MA)计算错误、临时限速未送至车载等。当系统出现复杂的多点故障时，可能无法保证行车安全。

在运行时验证中，预测上述危险的安全约束为：计算得到的系统可达集不包含超速或越过EoA的状态。这样，根据列车当前速度位置状态，如果验证满足安全约束，则可认为从当前状态直至停车，在所有可能运行工况的情况下，列车不会出现危险；反之，则认为列车存在危险的可能。

3 仿真验证

以北京燕房线为例，通过注入故障，验证所提出方法的有效性。

基于上述方法，利用混成自动机模型检验器SpaceEx开发了运行时验证系统。该系统独立于所监视的FAO系统运行。在每个系统控制周期中，监视器从不同的子系统接收重要的接口数据:从相应的传感器接收到列车速度和位置，从ZC接收到EoA位置。运行时验证系统中配置了线路拓扑结构，根据线路拓扑结构将列车位置和EoA位置转换为MA长度。在给定MA条件下，计算EBI和目标速度曲线，据此配置模型参数。运行时验证系统进而调用SpaceEx来计算列车速度位置(S,V)可达集。如果可达集包含S=MA且V>0的状态，则运行时验证系统报告危险，表明列车有可能超过EoA。如果可达集中不包含危险状态，监控器报告安全，表明列车在当前运行状态下没有潜在的危险。

3.1 危险场景设计

本文以下述2个危险场景为例，通过在FAO仿真平台中注入故障，验证所设计的运行时验证系统的有效性。

错误的坡度(IGt)。坡度列车运行中一个重要的附加阻力来源，通过对FAO系统中坡度数据注入故障，导致出现列车越过EoA。

错误的MA长度(ILMA)。通过不同方式注入错误MA长度故障，线路数据中注入故障、MA长度计算模块中注入错误以及联锁与ZC接口中注入故障，这些错误导致FAO车载系统依据错误的MA行车，最终导致列车越过EoA。

3.2 仿真试验结果及分析

运行时验证系统的仿真试验结果如表1所示。

表1 不同场景下的预测结果Tab.1 Predicted results in different scenarios

表1中，第一列显示了评估的CBTC场景，包括一个正常的执行场景和4个危险场景，每个场景都涉及上述危险之一。第2～5列为FAO车载运行数据，其中ST为列车位置，V为列车速度，SEoA为EoA位置，Gt为线路坡度。Pha表示列车运行阶段，其中Acc、Coa和Bak分别代表加速、惰行和制动。ResRV和ResATC分别表示部署运行时验证系统和不部署运行时验证系统的列车运行结果。由于验证需要消耗时间，当列车运行状态出现危险时，监控器报警信息存在延时。表1中t为运行时验证系统所需的运算时间，SA表示收到报警信号时列车的实际位置。

在正常的场景，运行时验证系统未给出危险信号，表明该系统未发生误报情况。

在IGt场景中，FAO系统使用了错误线路坡度18‰控制列车运行，而实际线路坡度为-18‰。在该场景中，当列车以21.1 m/s的速度行驶至1891.52 m的位置时，运行时验证系统预测出危险（在该状态之前，如果列车实施制动则可在EoA前停车）。该状态的可达集如图4所示，验证时间为6.03 s，此时列车已行驶至2018.75 m的位置。

图4 运行时验证可达集计算结果Fig.4 Calculation result of reachable set of runtime verification

收到危险信号开始制动，最终在EoA前停车。

在（21.1 m/s，1891.52 m）之后的每个列车运行状态，运行验证系统均预测存在危险。列车最早收到的警报是当列车位置位于1926.1 m和速度21.1 m/s的状态下。基于该状态运行时验证系统花费2.01 s计算可达集，列车行驶至1968.45 m时收到报警信息并开始实施制动，最终停在EoA之前。系统的运行过程如图5所示。

图5 运行时验证实施效果对比Fig.5 Comparison of implementation results of runtime verification

4 总结

本文提出了一种面向FAO系统的在线危险预测技术，通过构建运行时验证系统实现对真实系统运行时行为的可信性验证。该技术基于形式化模型，完备的计算列车从当前时刻至停车时刻的速度位置状态可达集，进而实现对行车危险的预测。实验结果表明,本文所述技术可有效预测FAO系统运行危险，避免了传统形式化方法对大规模系统的可验证性问题，为系统的实验室安全性验证提供一种有效手段。