基于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能否確保列車在其有效區段內安全行駛?，F雖有嚴格的調度管理機制和報文實時組幀技術來確保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契約模型的報文驗證能夠準確、全面、高效地識別報文數據的失效模式，提高了報文數據的正確率，且縮短了整個列控系統測試和驗證時間。