基于CPTA实现报文数据与车载系统契约关系的研究

王彤典，唐 涛

(北京交通大学 轨道交通控制与安全国家重点实验室,北京 100044)

CTCS-2级列控系统是安全苛求的数据驱动系统，车载系统解析线路数据后，需使用其计算控车模式曲线，从而驱动列车安全运行。列车的运行环境中存在着复杂的耦合因素，包括运营场景、车载型号参数、调度和列控中心等，都会对来自地面的数据有各自的要求；而地面数据不仅是数值的集合，其内涵是约束车载系统的行为。综上可知，报文数据与其宿主车载系统间存在相互制约的契约关系。因此若要保证报文能够约束系统实现安全功能，单纯地依靠数据供应链逐层验证的方式是不完备的，如图1所示，由于无法确保交付的数据能否满足系统需求，就有可能产生数据与系统需求不一致的隐患，带来不可接受的风险。在轨道交通领域，由于表征列车占用状态的数据没有被及时更新，导致车载系统使用后生成错误的控车曲线，造成“7·23”事故的发生[1]。2014年遂渝线动车组异常停车，因为报文数据描述范围不足造成D9类事故。2015年，在航空领域，由于配置了错误的降落点坐标，导致土耳其A330航班在降落时冲出跑道[2]。以上事故均是由于数据与系统功能需求不一致而导致的。针对此问题，国内外研究人员提出了不同的解决方案，英国安全苛求系统组织SCSC提出从数据消费者角度对数据进行约束[2]；文献[3]构建了列控数据层次模型，提出通过数据与系统的交互导出数据完整性需求；文献[4]建议在系统运行之前对所有可能的数据组合进行预验证，从而判断其是否能够驱动系统实现安全功能；文献[5]提出对IMS系统数据的开发及配置过程证明的思路[5]。国内相关研究主要是从数据逻辑关系和拓扑结构等角度验证数据的正确性[6-8]。以上成果推动了数据安全研究的进展，但多集中于航天和城轨CBTC领域，研究深度与实用性略显不足，且尚未发现以CTCS-2级列控车载与地面数据间契约关系视角来开展报文验证的研究。

图1 数据与宿主软件间不一致隐患的产生与传播

报文验证过程是：首先由报文工程师交叉检验，然后进行室内报文-车载静态仿真验证，最后完成不同运营场景下的联调联试。这个过程存在以下不足：

(1)缺少清晰、完备的报文验证规范。现有原则[9]存在部分内容表述模糊、不准确，且无法全面覆盖现场的各种线路情况，加之报文与车载研发人员立足于各自需求，对特殊情况的处理缺乏交流，因而对同一套规范的理解存在主观性。

(2)缺少对报文和车载一致性验证的形式化方法。虽然可以通过报文可视化、用户数据表一致性比对等方式验证报文的正确性和有效性[10]，且能够在一定程度上减少报文编制的失误，但却无法识别由于报文数据与系统需求不一致而产生的隐患。

报文验证的根本是判断其是否充分满足数据消费者，即ATP超速防护功能的安全实现对报文所提出的需求。

根据以上分析，本文提出基于环境的概率时间自动机CPTA(Context-based Probabilistic Timed Automata)形式化方法来构建报文与CTCS-2级车载ATP间的契约模型。图2给出本文的整体研究框架：首先分析了车载如何在不同运行环境下使用报文数据生成控车曲线，并对该过程进行FMEA分析，识别报文可能存在的失效模式及其对车载系统的影响；在此基础上，分别从数据语法、语义和时效性三方面提取ATP对报文应有的约束规则；然后借助CPTA模型描述在该数据约束条件下的车载状态迁移过程，并借助PVS定理证明机制证明该契约模型的正确性；最后设计了两组实验，通过与传统室内静态和室外动态报文验证对比，说明了该契约模型报文验证的可行性和高效性。

图2 基于CPTA方法实现报文-车载契约关系的形式化建模

1 报文与车载系统交互过程的安全分析

CTCS-2级列控系统车载设备与地面应答器之间的信息传递是单向的，即车载默认接收到的报文是正确且有效的，不会对报文数据实施校验，这恰忽视了该过程中的一致性匹配问题。例如：C2某线路在运营过程中曾有，每当列车侧线发车经过进站应答器JZ时，都会从完全监控模式FS转为部分监控模式PS，并以45 km/h速度通过，严重影响车站的通过效率。经反复排查发现，这是由于区间应答器Q的C1信息包变量NID_SIGNAL未按照车载处理逻辑编制导致的，而这类隐患在报文独立编制和验证阶段难以被发现。

通过剖析车载计算机在不同环境下使用报文生成速度-距离曲线的原理和过程，采用故障模式和影响分析方法FMEA对报文与车载的契约关系进行安全分析，识别出报文的失效模式以及对列控系统的影响，根据两者的结果，针对性地提取报文验证的约束规则。

1.1 基于报文数据计算速度-距离监控曲线

列控车载系统的核心功能是速度防护，基本过程为：车载系统接收地面设备传递的目标距离和目标速度，结合列车参数计算当前速度和位置，得到列车的允许速度。在该过程中，报文数据的主要作用是提供线路限速、坡度、闭塞分区长度、应答器和信号机位置等信息来辅助车载计算控车曲线，主要分为以下两部分。

(1)计算MRSP(Most Restrictive Speed Profile)曲线。ATP车载根据线路固定限速V_STATIC、机车构造速度、列车最大运行速度V_DIFF和临时限速TSR等参数确定列车的最限制速度曲线MRSP，如图3所示。且为了增加安全冗余距离，当列车进入减速和升速区段时，需分别考虑安全距离D和车长L对速度曲线的影响，在MRSP曲线的基础上，可进一步得到常用制动曲线MRSPNBP。

图3 车载工作周期内超速防护曲线计算原理

(2)计算目标-距离控车曲线。目标-距离控制曲线是在MRSPNBP基础上依据列车安全制动模型得到的，由顶棚速度曲线CSM和目标速度曲线TSM两部分组成。如图3所示，当列车经过应答器Q1时，会根据其发送的L_SECTION(前方空闲闭塞分区长度L1～L7)，连同轨道电路信息码计算出目标距离Stgt，再分段计算TSM曲线。以Stgt1为例，设减速度、初速和末速分别为a1,VL1,VL2，若列车在P1处开始制动，首先根据式( 1 )计算空走距离Sk，而后根据列车制动模型式( 2 )计算制动距离Se，车载最终根据行车许可MA位置、MRSPNBP、模式曲线计算公式( 3 )和系统配置参数k等计算出速度-距离监控曲线，如图4所示。

( 1 )

( 2 )

( 3 )

图4 计算速度监控曲线流程

1.2 基于FMEA实现契约关系的安全分析

使用FMEA方法对报文与车载ATP间的契约关系进行表1所示的安全分析，得到当报文数据不满足车载安全需求时的失效模式，并分析了该失效模式可能出现的原因和后果，为后续提取报文安全性约束提供依据。

表1 报文与车载间契约关系的FMEA分析

现行预防措施主要有：M1，预判工程数据表的完整性，正确、及时地接续；M2，依照报文工程师经验确定应答器信息包内容；M3，根据现场调试经验限制合包范围和长度；M4，开发基于ATP硬件环境的报文仿真测试平台验证报文；M5，LEU采用连续不间断的方式向有源应答器发送报文。

数据失效产生的原因是报文未能正确描述列车运行所需线路信息的状态，即没有满足车载安全运行的需求。更进一步讲，ATP运行环境复杂多变，环境中各要素间相互制约，存在着复杂的耦合关系，且都对来自地面的报文数据有不同的需求，如调度中心会要求临时限速的正确性和时效性、不同发车进路会对CTCS-1信息包变量NID_SIGNAL有相应的要求等，而列控车载系统正是基于环境因素对数据诸如此类的需求，结合自身牵引和制动性能等最终计算得到速度-距离控制曲线。因此，首先需要提取各类环境因素对报文数据的安全约束，即车载默认的、理想的报文所应满足的规则。

2 基于车载运行环境构建报文安全性约束

本文以下行线侧线接车场景为例来分析该过程中对报文数据的安全性约束。如图5所示，该线路上配置的应答器包括区间应答器Q、定位应答器DW、进站应答器JZ、反出站应答器FCZ和出站应答器CZ，各应答器会根据车载运行环境需求发送相应的信息包，因此首先将环境C中各耦合因素分离为以下4类：运行场景Scnr={区间行驶、侧线接车、侧线发车}，调度命令Disp={CTCS-2临时限速信息、接发车进路}，线路条件LineData={轨道区段、坡度、速度、信号机、应答器、分相区、接发车进路、断链}，车载性能Perf={制动模型、牵引模型、最大列车速度、车长}。列车运行环境C={Scnr,Disp,LineData,Pef}。综合考虑各环境因素对线路报文的安全需求后，可将其安全性约束分为三类：语法约束用来判断数据属性域值是否正确，属性精度是否合法，即确保所给报文数据自身的正确性和完备性；语义约束用来判断所给报文数据能否驱动车载安全运行，即确保报文能安全地约束系统；时效性约束用来确保报文验证结果能够及时传递给车载。

图5 下行侧线接车进路

之后将这三类约束使用PVS高阶逻辑进行形式化规约，作为后续构建CPTA契约模型的基础。原型验证系统PVS(Prototype Verification System)[11-12]拥有基于高阶逻辑的形式化规约体系，可以通过丰富的数据类型系统表达任意形式和复杂度的数据逻辑约束。

2.1 报文语法模式需求

语法模式是指对报文信息逻辑结构和特征的描述，包括数据自身属性约束，包含变量类型、取值范围等，以及与数据有关的有效性和完整性要求。实际中经常会出现由于数据描述范围不足、变量值编写错误等引发的列车提前降速或制动，严重影响运行效率。因此需要根据列车实际运行环境分别从报文完备性、一致性和正确性角度提取相应的需求，并将其形式化为相应的PVS公理。

2.1.1 报文完备性

报文数据的完备性是指线路数据的维度是否正确，提供的信息是否完整，即各信息包的数据覆盖范围是否充足。应答器报文的覆盖范围是安全行车的重要依据，一旦应答器丢失或故障，冗余的覆盖范围可以保证列车继续安全行驶。尽管文献[9]已经规定了轨道区段、速度、坡度等信息包的数据范围，但在动态调试或实际运营中仍会发生由于缺少数据而导致列车异常制动的事件，这是因为地面数据开发人员无法确认所给数据范围是否满足车载生成控车曲线的要求。下面以图5所示进路中应答器Q1的CTCS-1轨道区段信息包和应答器CZ的CTCS-2临时限速信息包为例进行剖析。

(1)CTCS-1数据覆盖范围

列车在Q1处收到L5码被告知前方有7个闭塞分区空闲，此时CTCS-1包的L_SECTION变量会告知车载每个闭塞分区的长度。为了实现侧线安全接车，MA停车终点必须在出站信号机处，因此C1包的覆盖范围必须至前方第7个闭塞分区末端，即从本应答器开始至前方第二个Q2再延长一个数据余量L，如此才能够确保生成正确的动态监控曲线。

(2)CTCS-2数据覆盖范围

当列车进站时，会收到有源应答器JZ发送的CTCS-2临时限速信息，包括临时限速有效区段长度L_TSRarea、临时限速值TSR。本文运营场景中，TSR为45 km/h，L_TSRarea为进站口至出站延长80 m[13]，如图5所示。将其形式化为PVS公理TelegramCover，其中，ptC1,ptE21,ptE27,ptC2表示车载接收到的信息包，函数pred_LinkLen用于计算信息包的覆盖范围TeleCovLen。

TelegramCover:AXIOM

TeleCovCorrect？ [Telegram,TeleCov]:RECURSIVEbool=

∀((ptC1,ptE21,ptE27,ptC2:t)∈Telegram:list[TeleVar]) ⟹

(TeleCovLen(t)=LinkLen+DataMargin)∧(TeleCovLen(t)=Locexit-Locentrance+80 m)

IFTeleCovLen(t)>Stgt_LenTHEN (TeleCovCorrect=TRUE)

pred_LinkLen[Q_Loc->L_Len]:TYPE=(LAMADA(f:[Q_Loc->L_Len]):

(∀(LocQ_Balise:Q_Loc) ⟹(LinkLen=LocQ_Balise-LocQ_BaliseFormer))

2.1.2 报文一致性

报文一致性约束用来确保ETCS-5信息包的有效性。车载系统通过ETCS-5信息包传递的链接信息，能够及时识别是否有应答器丢失或损坏；同时还可以根据E5包的应答器编号NID_BG，以及链接距离D_LINK消除累计的测速测距误差，并校正列车位置。下面以应答器链接一致性为例进行分析。

(1)链接一致性

列车经过应答器Q1时会收到ETCS-5应答器链接信息包，包括前方被链接应答器的位置D_LINK、链接应答器允许的安装偏差Q_LOCACC等，CTCS-2车载会根据该信息计算期望应答器窗口长度E=|Q_LINKACC+D_LINK·0.02|。如图6所示，如果车载收到应答器Q2-1的位置是在期望窗口E之前，或是在列车越过期望窗口300 ms后还未收到信息包，则证明应答器组链接一致性错误，车载应根据从Q1收到的信息Q_LINKREACTION执行链接反应。一般情况下，Q_LINKREACTION=“无反应”，但当E5链接了出站信号机旁的有源应答器(包含禁止报文)时，ATP控车可能存在不安全因素，则Q_LINKREACTION=“紧急制动”。形式化为LinkConsist公理：

LinkConsist:AXIOM

ETCS_5_Correct？ [Balise,E5_Loc]:RECURSIVEbool=

∀(ETCS_5⊂((PassiveBalise.Packet)∧(ActiveBalise.Packet)))⟹

(E_Len

(IF (LinkInconsistFORCZ) THEN (Q_REACTIONLINK=‘Brake’)

ELSE (Q_REACTIONLINK=‘NO_Action’))

pred_Cal_E_Len[Var->E_Len]:TYPE=(LAMADA(f:[Var->E_Len]):

(∀(Var:ETCS_5)⟹(E_Len=Q_LOCACC+D_LINK·0.02))

图6 链接应答器期望窗口计算

2.1.3 报文正确性

报文完备性和一致性约束确保ATP能够在预期的位置收到完整的报文数据。正确性约束用来验证报文数据属性值范围、属性间逻辑关系是否正确，如速度、坡度值范围是否超出最大值、断链位置是否与速度点一致以及信息包变量值是否合法等。

超包与合包。当线路过长或过于复杂时，报文编制有可能会出现超包现象，即应答器信息包位数超过最大容量830 bit，此时可对CTCS-1轨道区段的L_SECTION变量，以及ETCS-21线路坡度的G_A变量进行合并。如图7所示，当列车经过应答器Q2时，车载系统会收到C1包描述的前方空闲轨道区段长度L1～L11。若出现超包，则需由远及近地合并L1～L11中“没有信号机”，从而得到新的轨道区段信息l1～l5，且合并后长度需在数据余量L范围内。

图7 合并CTCS-1信息包的轨道区段长度L_SECTION变量

2.2 报文功能语义需求

报文数据语义是指对数据内涵的约束，使得该数据能够驱动车载系统实现安全功能。上文总结的报文语法模式约束，能够识别出数据范围不足、合包超位等数据隐患，从而确保报文的逻辑结构和特征能够满足车载超速防护功能的需求。然而，这仍无法验证动态报文的数据语义能否满足ATP控车需求，以临时限速变量TSR为例，即无法判定当前接收到的TSR能否确保列车在其有效区段内安全行驶。现虽有严格的调度管理机制和报文实时组帧技术来确保TSR下发过程的安全性，但仍需较多的人工干预，正如文献[14]所说，人因失效导致的工业、企业事故率高达80%以上，且根据表1对契约模型FMEA分析可知，一旦人员疏忽致使TSR选择或编制错误，则会带来不可接受的风险。因此，本文提出朴素贝叶斯算法预判动态数据语义的可信度。

( 4 )

( 5 )

( 6 )

( 7 )

(2)计算参数φ,μ,ε的极大似然估计。为了拟合得到贝叶斯模型参数，需借助极大似然公式求解参数φ,μ,ε。首先将式( 5 )～式( 7 )分别带入式( 4 )后得到式( 8 )，然后求各临时限速值的联合分布，两边同时取In导数得到式( 9 )，求解得到各参数计算式(10)。将参数φ,μ,ε分别带入式( 8 )即可得到当前环境下，每类临时限速出现的可能性，从而实现对临时限速语义可信度的计算。

( 8 )

( 9 )

(10)

2.3 报文时效性需求

列控系统是典型的实时系统，需要在有效时间内对报文做出实时响应，因而报文与车载契约模型的事务特征之一是“时效性”，即在报文与车载双向交互的仿真实验中，车载提出对报文的需求，而报文需在有效时间tvalid内给予反馈，且一旦超出tvalid，则说明报文错误或者丢失。举例来说：当列车准备侧线发车，且正线出站信号机旁设置了应答器CZ时，应答器Q接收到CTCS-1包后，车载发出对轨道区段长度NID_SIGNAL进行验证的请求，契约模型结合当前运行环境，约定只有当该变量满足NID_SIGNAL=0111 &T_SectionVerify

上述是以车载ATP计算控车曲线作为需求，分别从报文信息包语法模式、功能语义和时效性三方面提出了相应的公理约束，如TelegramCover等，作为CPTA形式化建模和验证的基础。

3 基于CPTA实现车地契约关系的形式化建模与验证

将报文语法、语义和时效性三部分约束作为系统状态迁移的条件，不仅能够实时反映出报文与车载的交互状态，且一旦出现报文信息包无法满足车载的一致性需求时，还可以及时得到不一致发生的原因，以及对车载的影响。举例来说，图8为当车载接收到CTCS-2包中的临时限速后，在T11时间内计算出当前环境下限速值出现的可能性为0.9，因此列车会按照调度下发的该限速值安全行驶。下面就以临时限速数据为例对报文-车载契约关系进行建模。

图8 基于CPTA的报文-车载契约模型图形化描述示例

3.1 基于CPTA构建报文-车载的契约模型

当车载经过应答器接收到相应的信息包后，会发出对报文验证的请求，契约模型接收到该请求后，分别验证报文的语法、语义和时效性，并将验证结果同车载请求进行一致性比对，若两者一致，则代表该数据符合车载的安全性需求。图9描述了车载ATP在计算MRSP曲线过程中对临时限速的验证过程，其中，图9(a)表示车载ATP对临时限速的验证过程，图9(b)表示契约模型验证临时限速可信度的过程。

图9 基于CPTA验证线路限速数据过程

当ATP发出TSR_Check!请求后，契约模型调取TSR_ReliaJudge约束对临时限速的可信度R进行计算，然后向车载反馈TSRCorrect!命令。车载接收到TSRCorrect?命令后，根据数据的可信度执行从状态S_TSR到S_TSR_Receive的转换。

本文提出的CPTA方法论旨在通过实时准确地描述列车在不同运行场景中与报文数据的交互过程，来定性分离环境中的耦合因素，并从语法、语义和时效三方面定量刻画出其对报文的约束，将其映射为车载系统状态迁移的条件，从而实现了车载解析并使用报文的可视化过程。

3.2 结果分析

为了证实CPTA契约模型验证报文的有效性和实用性，本文基于上述报文数据约束规则和契约模型，在Visual Studio 2010环境中开发了基于CPTA契约模型的报文验证软件，并设计了两组实验，分别从报文验证性能和效率两方面，与以往报文室内静态仿真验证和室外动态调试进行对比。

实验一选取某信号设备研发公司的20条C2线路原始报文作为报文验证软件的实验数据，同时收集该线路以往室内静态验证和室外动调过程中，由于报文失效造成的列车异常制动或降速次数，作为参考数据进行对比。实验二选择复杂度递增的3条C2线路作为实验数据，对基于CPTA契约模型报文验证、传统室内报文静态验证和室外动调三种方式的验证时间进行对比，且为了能够合理表现室外动态调试时间，将实际动调时间缩小10倍，如图10、图11所示。

图10 线路条数对列车异常制动次数的影响

图10结果表明基于CPTA契约模型验证报文几乎能够达到室外动态调试的效果，能够识别传统静态报文仿真验证无法识别的报文失效模式，如合包后轨道区段长度过长、应答器JL信息不完备等。虽仍未能全面识别出所有的报文失效模式，但相比室内报文验证而言，已经明显提高了报文验证的可靠性。图11结果表明基于CPTA契约模型的报文验证时间远小于动态调试时间，略大于室内静态报文仿真时间。随着线路复杂度提升，验证时间有所增加，但由于基于契约模型的报文验证属于线下验证，这属于可接受范围，且从系统角度来看，该方法减少了整个列控系统调试和验证时间。

图11 线路复杂度对报文验证所需时间的影响

4 结论

本文根据报文与车载间存在的契约关系，提出一种新的报文验证方案，即通过构建基于环境的概率时间自动机CPTA模型来形式化描述CTCS-2级车载ATP与报文间的交互过程，实现完备且有效的报文验证。剖析了车载在不同运行环境下使用报文生成动态监控曲线的过程，并对该过程进行FMEA分析，识别得到报文可能存在的失效模式。分别从语法、语义和时效性三方面提取ATP对报文的需求，作为CPTA模型中车载状态迁移的条件，借助PVS定理证明工具证明了该契约模型的正确性。研究和实验结果表明：

(1)基于报文-车载契约关系提取的报文数据语法约束能够减少因数据范围不足、合包距离过长或信息包变量描述不一致等造成的列车异常制动或降速的次数，且通过报文语义约束能够及时发现TSR下发错误，并使列车导向安全侧。

(2)基于CPTA契约模型的报文验证能够准确、全面、高效地识别报文数据的失效模式，提高了报文数据的正确率，且缩短了整个列控系统测试和验证时间。