王彤典，唐 濤

(北京交通大學(xué) 軌道交通控制與安全國家重點實驗室,北京 100044)

CTCS-2級列控系統(tǒng)是安全苛求的數(shù)據(jù)驅(qū)動系統(tǒng)，車載系統(tǒng)解析線路數(shù)據(jù)后，需使用其計算控車模式曲線，從而驅(qū)動列車安全運(yùn)行。列車的運(yùn)行環(huán)境中存在著復(fù)雜的耦合因素，包括運(yùn)營場景、車載型號參數(shù)、調(diào)度和列控中心等，都會對來自地面的數(shù)據(jù)有各自的要求；而地面數(shù)據(jù)不僅是數(shù)值的集合，其內(nèi)涵是約束車載系統(tǒng)的行為。綜上可知，報文數(shù)據(jù)與其宿主車載系統(tǒng)間存在相互制約的契約關(guān)系。因此若要保證報文能夠約束系統(tǒng)實現(xiàn)安全功能，單純地依靠數(shù)據(jù)供應(yīng)鏈逐層驗證的方式是不完備的，如圖1所示，由于無法確保交付的數(shù)據(jù)能否滿足系統(tǒng)需求，就有可能產(chǎn)生數(shù)據(jù)與系統(tǒng)需求不一致的隱患，帶來不可接受的風(fēng)險。在軌道交通領(lǐng)域，由于表征列車占用狀態(tài)的數(shù)據(jù)沒有被及時更新，導(dǎo)致車載系統(tǒng)使用后生成錯誤的控車曲線，造成“7·23”事故的發(fā)生[1]。2014年遂渝線動車組異常停車，因為報文數(shù)據(jù)描述范圍不足造成D9類事故。2015年，在航空領(lǐng)域，由于配置了錯誤的降落點坐標(biāo)，導(dǎo)致土耳其A330航班在降落時沖出跑道[2]。以上事故均是由于數(shù)據(jù)與系統(tǒng)功能需求不一致而導(dǎo)致的。針對此問題，國內(nèi)外研究人員提出了不同的解決方案，英國安全苛求系統(tǒng)組織SCSC提出從數(shù)據(jù)消費者角度對數(shù)據(jù)進(jìn)行約束[2]；文獻(xiàn)[3]構(gòu)建了列控數(shù)據(jù)層次模型，提出通過數(shù)據(jù)與系統(tǒng)的交互導(dǎo)出數(shù)據(jù)完整性需求；文獻(xiàn)[4]建議在系統(tǒng)運(yùn)行之前對所有可能的數(shù)據(jù)組合進(jìn)行預(yù)驗證，從而判斷其是否能夠驅(qū)動系統(tǒng)實現(xiàn)安全功能；文獻(xiàn)[5]提出對IMS系統(tǒng)數(shù)據(jù)的開發(fā)及配置過程證明的思路[5]。國內(nèi)相關(guān)研究主要是從數(shù)據(jù)邏輯關(guān)系和拓?fù)浣Y(jié)構(gòu)等角度驗證數(shù)據(jù)的正確性[6-8]。以上成果推動了數(shù)據(jù)安全研究的進(jìn)展，但多集中于航天和城軌CBTC領(lǐng)域，研究深度與實用性略顯不足，且尚未發(fā)現(xiàn)以CTCS-2級列控車載與地面數(shù)據(jù)間契約關(guān)系視角來開展報文驗證的研究。

圖1 數(shù)據(jù)與宿主軟件間不一致隱患的產(chǎn)生與傳播

報文驗證過程是：首先由報文工程師交叉檢驗，然后進(jìn)行室內(nèi)報文-車載靜態(tài)仿真驗證，最后完成不同運(yùn)營場景下的聯(lián)調(diào)聯(lián)試。這個過程存在以下不足：

(1)缺少清晰、完備的報文驗證規(guī)范?，F(xiàn)有原則[9]存在部分內(nèi)容表述模糊、不準(zhǔn)確，且無法全面覆蓋現(xiàn)場的各種線路情況，加之報文與車載研發(fā)人員立足于各自需求，對特殊情況的處理缺乏交流，因而對同一套規(guī)范的理解存在主觀性。

(2)缺少對報文和車載一致性驗證的形式化方法。雖然可以通過報文可視化、用戶數(shù)據(jù)表一致性比對等方式驗證報文的正確性和有效性[10]，且能夠在一定程度上減少報文編制的失誤，但卻無法識別由于報文數(shù)據(jù)與系統(tǒng)需求不一致而產(chǎn)生的隱患。

報文驗證的根本是判斷其是否充分滿足數(shù)據(jù)消費者，即ATP超速防護(hù)功能的安全實現(xiàn)對報文所提出的需求。

根據(jù)以上分析，本文提出基于環(huán)境的概率時間自動機(jī)CPTA(Context-based Probabilistic Timed Automata)形式化方法來構(gòu)建報文與CTCS-2級車載ATP間的契約模型。圖2給出本文的整體研究框架：首先分析了車載如何在不同運(yùn)行環(huán)境下使用報文數(shù)據(jù)生成控車曲線，并對該過程進(jìn)行FMEA分析，識別報文可能存在的失效模式及其對車載系統(tǒng)的影響；在此基礎(chǔ)上，分別從數(shù)據(jù)語法、語義和時效性三方面提取ATP對報文應(yīng)有的約束規(guī)則；然后借助CPTA模型描述在該數(shù)據(jù)約束條件下的車載狀態(tài)遷移過程，并借助PVS定理證明機(jī)制證明該契約模型的正確性；最后設(shè)計了兩組實驗，通過與傳統(tǒng)室內(nèi)靜態(tài)和室外動態(tài)報文驗證對比，說明了該契約模型報文驗證的可行性和高效性。

圖2 基于CPTA方法實現(xiàn)報文-車載契約關(guān)系的形式化建模

1 報文與車載系統(tǒng)交互過程的安全分析

CTCS-2級列控系統(tǒng)車載設(shè)備與地面應(yīng)答器之間的信息傳遞是單向的，即車載默認(rèn)接收到的報文是正確且有效的，不會對報文數(shù)據(jù)實施校驗，這恰忽視了該過程中的一致性匹配問題。例如：C2某線路在運(yùn)營過程中曾有，每當(dāng)列車側(cè)線發(fā)車經(jīng)過進(jìn)站應(yīng)答器JZ時，都會從完全監(jiān)控模式FS轉(zhuǎn)為部分監(jiān)控模式PS，并以45 km/h速度通過，嚴(yán)重影響車站的通過效率。經(jīng)反復(fù)排查發(fā)現(xiàn)，這是由于區(qū)間應(yīng)答器Q的C1信息包變量NID_SIGNAL未按照車載處理邏輯編制導(dǎo)致的，而這類隱患在報文獨立編制和驗證階段難以被發(fā)現(xiàn)。

通過剖析車載計算機(jī)在不同環(huán)境下使用報文生成速度-距離曲線的原理和過程，采用故障模式和影響分析方法FMEA對報文與車載的契約關(guān)系進(jìn)行安全分析，識別出報文的失效模式以及對列控系統(tǒng)的影響，根據(jù)兩者的結(jié)果，針對性地提取報文驗證的約束規(guī)則。

1.1 基于報文數(shù)據(jù)計算速度-距離監(jiān)控曲線

列控車載系統(tǒng)的核心功能是速度防護(hù)，基本過程為：車載系統(tǒng)接收地面設(shè)備傳遞的目標(biāo)距離和目標(biāo)速度，結(jié)合列車參數(shù)計算當(dāng)前速度和位置，得到列車的允許速度。在該過程中，報文數(shù)據(jù)的主要作用是提供線路限速、坡度、閉塞分區(qū)長度、應(yīng)答器和信號機(jī)位置等信息來輔助車載計算控車曲線，主要分為以下兩部分。

(1)計算MRSP(Most Restrictive Speed Profile)曲線。ATP車載根據(jù)線路固定限速V_STATIC、機(jī)車構(gòu)造速度、列車最大運(yùn)行速度V_DIFF和臨時限速TSR等參數(shù)確定列車的最限制速度曲線MRSP，如圖3所示。且為了增加安全冗余距離，當(dāng)列車進(jìn)入減速和升速區(qū)段時，需分別考慮安全距離D和車長L對速度曲線的影響，在MRSP曲線的基礎(chǔ)上，可進(jìn)一步得到常用制動曲線MRSPNBP。

圖3 車載工作周期內(nèi)超速防護(hù)曲線計算原理

(2)計算目標(biāo)-距離控車曲線。目標(biāo)-距離控制曲線是在MRSPNBP基礎(chǔ)上依據(jù)列車安全制動模型得到的，由頂棚速度曲線CSM和目標(biāo)速度曲線TSM兩部分組成。如圖3所示，當(dāng)列車經(jīng)過應(yīng)答器Q1時，會根據(jù)其發(fā)送的L_SECTION(前方空閑閉塞分區(qū)長度L1～L7)，連同軌道電路信息碼計算出目標(biāo)距離Stgt，再分段計算TSM曲線。以Stgt1為例，設(shè)減速度、初速和末速分別為a1,VL1,VL2，若列車在P1處開始制動，首先根據(jù)式( 1 )計算空走距離Sk，而后根據(jù)列車制動模型式( 2 )計算制動距離Se，車載最終根據(jù)行車許可MA位置、MRSPNBP、模式曲線計算公式( 3 )和系統(tǒng)配置參數(shù)k等計算出速度-距離監(jiān)控曲線，如圖4所示。

( 1 )

( 2 )

( 3 )

圖4 計算速度監(jiān)控曲線流程

1.2 基于FMEA實現(xiàn)契約關(guān)系的安全分析

使用FMEA方法對報文與車載ATP間的契約關(guān)系進(jìn)行表1所示的安全分析，得到當(dāng)報文數(shù)據(jù)不滿足車載安全需求時的失效模式，并分析了該失效模式可能出現(xiàn)的原因和后果，為后續(xù)提取報文安全性約束提供依據(jù)。

表1 報文與車載間契約關(guān)系的FMEA分析

現(xiàn)行預(yù)防措施主要有：M1，預(yù)判工程數(shù)據(jù)表的完整性，正確、及時地接續(xù)；M2，依照報文工程師經(jīng)驗確定應(yīng)答器信息包內(nèi)容；M3，根據(jù)現(xiàn)場調(diào)試經(jīng)驗限制合包范圍和長度；M4，開發(fā)基于ATP硬件環(huán)境的報文仿真測試平臺驗證報文；M5，LEU采用連續(xù)不間斷的方式向有源應(yīng)答器發(fā)送報文。

數(shù)據(jù)失效產(chǎn)生的原因是報文未能正確描述列車運(yùn)行所需線路信息的狀態(tài)，即沒有滿足車載安全運(yùn)行的需求。更進(jìn)一步講，ATP運(yùn)行環(huán)境復(fù)雜多變，環(huán)境中各要素間相互制約，存在著復(fù)雜的耦合關(guān)系，且都對來自地面的報文數(shù)據(jù)有不同的需求，如調(diào)度中心會要求臨時限速的正確性和時效性、不同發(fā)車進(jìn)路會對CTCS-1信息包變量NID_SIGNAL有相應(yīng)的要求等，而列控車載系統(tǒng)正是基于環(huán)境因素對數(shù)據(jù)諸如此類的需求，結(jié)合自身牽引和制動性能等最終計算得到速度-距離控制曲線。因此，首先需要提取各類環(huán)境因素對報文數(shù)據(jù)的安全約束，即車載默認(rèn)的、理想的報文所應(yīng)滿足的規(guī)則。

2 基于車載運(yùn)行環(huán)境構(gòu)建報文安全性約束

本文以下行線側(cè)線接車場景為例來分析該過程中對報文數(shù)據(jù)的安全性約束。如圖5所示，該線路上配置的應(yīng)答器包括區(qū)間應(yīng)答器Q、定位應(yīng)答器DW、進(jìn)站應(yīng)答器JZ、反出站應(yīng)答器FCZ和出站應(yīng)答器CZ，各應(yīng)答器會根據(jù)車載運(yùn)行環(huán)境需求發(fā)送相應(yīng)的信息包，因此首先將環(huán)境C中各耦合因素分離為以下4類：運(yùn)行場景Scnr={區(qū)間行駛、側(cè)線接車、側(cè)線發(fā)車}，調(diào)度命令Disp={CTCS-2臨時限速信息、接發(fā)車進(jìn)路}，線路條件LineData={軌道區(qū)段、坡度、速度、信號機(jī)、應(yīng)答器、分相區(qū)、接發(fā)車進(jìn)路、斷鏈}，車載性能Perf={制動模型、牽引模型、最大列車速度、車長}。列車運(yùn)行環(huán)境C={Scnr,Disp,LineData,Pef}。綜合考慮各環(huán)境因素對線路報文的安全需求后，可將其安全性約束分為三類：語法約束用來判斷數(shù)據(jù)屬性域值是否正確，屬性精度是否合法，即確保所給報文數(shù)據(jù)自身的正確性和完備性；語義約束用來判斷所給報文數(shù)據(jù)能否驅(qū)動車載安全運(yùn)行，即確保報文能安全地約束系統(tǒng)；時效性約束用來確保報文驗證結(jié)果能夠及時傳遞給車載。

圖5 下行側(cè)線接車進(jìn)路

之后將這三類約束使用PVS高階邏輯進(jìn)行形式化規(guī)約，作為后續(xù)構(gòu)建CPTA契約模型的基礎(chǔ)。原型驗證系統(tǒng)PVS(Prototype Verification System)[11-12]擁有基于高階邏輯的形式化規(guī)約體系，可以通過豐富的數(shù)據(jù)類型系統(tǒng)表達(dá)任意形式和復(fù)雜度的數(shù)據(jù)邏輯約束。

2.1 報文語法模式需求

語法模式是指對報文信息邏輯結(jié)構(gòu)和特征的描述，包括數(shù)據(jù)自身屬性約束，包含變量類型、取值范圍等，以及與數(shù)據(jù)有關(guān)的有效性和完整性要求。實際中經(jīng)常會出現(xiàn)由于數(shù)據(jù)描述范圍不足、變量值編寫錯誤等引發(fā)的列車提前降速或制動，嚴(yán)重影響運(yùn)行效率。因此需要根據(jù)列車實際運(yùn)行環(huán)境分別從報文完備性、一致性和正確性角度提取相應(yīng)的需求，并將其形式化為相應(yīng)的PVS公理。

2.1.1 報文完備性

報文數(shù)據(jù)的完備性是指線路數(shù)據(jù)的維度是否正確，提供的信息是否完整，即各信息包的數(shù)據(jù)覆蓋范圍是否充足。應(yīng)答器報文的覆蓋范圍是安全行車的重要依據(jù)，一旦應(yīng)答器丟失或故障，冗余的覆蓋范圍可以保證列車?yán)^續(xù)安全行駛。盡管文獻(xiàn)[9]已經(jīng)規(guī)定了軌道區(qū)段、速度、坡度等信息包的數(shù)據(jù)范圍，但在動態(tài)調(diào)試或?qū)嶋H運(yùn)營中仍會發(fā)生由于缺少數(shù)據(jù)而導(dǎo)致列車異常制動的事件，這是因為地面數(shù)據(jù)開發(fā)人員無法確認(rèn)所給數(shù)據(jù)范圍是否滿足車載生成控車曲線的要求。下面以圖5所示進(jìn)路中應(yīng)答器Q1的CTCS-1軌道區(qū)段信息包和應(yīng)答器CZ的CTCS-2臨時限速信息包為例進(jìn)行剖析。

(1)CTCS-1數(shù)據(jù)覆蓋范圍

列車在Q1處收到L5碼被告知前方有7個閉塞分區(qū)空閑，此時CTCS-1包的L_SECTION變量會告知車載每個閉塞分區(qū)的長度。為了實現(xiàn)側(cè)線安全接車，MA停車終點必須在出站信號機(jī)處，因此C1包的覆蓋范圍必須至前方第7個閉塞分區(qū)末端，即從本應(yīng)答器開始至前方第二個Q2再延長一個數(shù)據(jù)余量L，如此才能夠確保生成正確的動態(tài)監(jiān)控曲線。

(2)CTCS-2數(shù)據(jù)覆蓋范圍

當(dāng)列車進(jìn)站時，會收到有源應(yīng)答器JZ發(fā)送的CTCS-2臨時限速信息，包括臨時限速有效區(qū)段長度L_TSRarea、臨時限速值TSR。本文運(yùn)營場景中，TSR為45 km/h，L_TSRarea為進(jìn)站口至出站延長80 m[13]，如圖5所示。將其形式化為PVS公理TelegramCover，其中，ptC1,ptE21,ptE27,ptC2表示車載接收到的信息包，函數(shù)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信息包的有效性。車載系統(tǒng)通過ETCS-5信息包傳遞的鏈接信息，能夠及時識別是否有應(yīng)答器丟失或損壞；同時還可以根據(jù)E5包的應(yīng)答器編號NID_BG，以及鏈接距離D_LINK消除累計的測速測距誤差，并校正列車位置。下面以應(yīng)答器鏈接一致性為例進(jìn)行分析。

(1)鏈接一致性

列車經(jīng)過應(yīng)答器Q1時會收到ETCS-5應(yīng)答器鏈接信息包，包括前方被鏈接應(yīng)答器的位置D_LINK、鏈接應(yīng)答器允許的安裝偏差Q_LOCACC等，CTCS-2車載會根據(jù)該信息計算期望應(yīng)答器窗口長度E=|Q_LINKACC+D_LINK·0.02|。如圖6所示，如果車載收到應(yīng)答器Q2-1的位置是在期望窗口E之前，或是在列車越過期望窗口300 ms后還未收到信息包，則證明應(yīng)答器組鏈接一致性錯誤，車載應(yīng)根據(jù)從Q1收到的信息Q_LINKREACTION執(zhí)行鏈接反應(yīng)。一般情況下，Q_LINKREACTION=“無反應(yīng)”，但當(dāng)E5鏈接了出站信號機(jī)旁的有源應(yīng)答器(包含禁止報文)時，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 鏈接應(yīng)答器期望窗口計算

2.1.3 報文正確性

報文完備性和一致性約束確保ATP能夠在預(yù)期的位置收到完整的報文數(shù)據(jù)。正確性約束用來驗證報文數(shù)據(jù)屬性值范圍、屬性間邏輯關(guān)系是否正確，如速度、坡度值范圍是否超出最大值、斷鏈位置是否與速度點一致以及信息包變量值是否合法等。

超包與合包。當(dāng)線路過長或過于復(fù)雜時，報文編制有可能會出現(xiàn)超包現(xiàn)象，即應(yīng)答器信息包位數(shù)超過最大容量830 bit，此時可對CTCS-1軌道區(qū)段的L_SECTION變量，以及ETCS-21線路坡度的G_A變量進(jìn)行合并。如圖7所示，當(dāng)列車經(jīng)過應(yīng)答器Q2時，車載系統(tǒng)會收到C1包描述的前方空閑軌道區(qū)段長度L1～L11。若出現(xiàn)超包，則需由遠(yuǎn)及近地合并L1～L11中“沒有信號機(jī)”，從而得到新的軌道區(qū)段信息l1～l5，且合并后長度需在數(shù)據(jù)余量L范圍內(nèi)。

圖7 合并CTCS-1信息包的軌道區(qū)段長度L_SECTION變量

2.2 報文功能語義需求

報文數(shù)據(jù)語義是指對數(shù)據(jù)內(nèi)涵的約束，使得該數(shù)據(jù)能夠驅(qū)動車載系統(tǒng)實現(xiàn)安全功能。上文總結(jié)的報文語法模式約束，能夠識別出數(shù)據(jù)范圍不足、合包超位等數(shù)據(jù)隱患，從而確保報文的邏輯結(jié)構(gòu)和特征能夠滿足車載超速防護(hù)功能的需求。然而，這仍無法驗證動態(tài)報文的數(shù)據(jù)語義能否滿足ATP控車需求，以臨時限速變量TSR為例，即無法判定當(dāng)前接收到的TSR能否確保列車在其有效區(qū)段內(nèi)安全行駛?，F(xiàn)雖有嚴(yán)格的調(diào)度管理機(jī)制和報文實時組幀技術(shù)來確保TSR下發(fā)過程的安全性，但仍需較多的人工干預(yù)，正如文獻(xiàn)[14]所說，人因失效導(dǎo)致的工業(yè)、企業(yè)事故率高達(dá)80%以上，且根據(jù)表1對契約模型FMEA分析可知，一旦人員疏忽致使TSR選擇或編制錯誤，則會帶來不可接受的風(fēng)險。因此，本文提出樸素貝葉斯算法預(yù)判動態(tài)數(shù)據(jù)語義的可信度。

( 4 )

( 5 )

( 6 )

( 7 )

(2)計算參數(shù)φ,μ,ε的極大似然估計。為了擬合得到貝葉斯模型參數(shù)，需借助極大似然公式求解參數(shù)φ,μ,ε。首先將式( 5 )～式( 7 )分別帶入式( 4 )后得到式( 8 )，然后求各臨時限速值的聯(lián)合分布，兩邊同時取In導(dǎo)數(shù)得到式( 9 )，求解得到各參數(shù)計算式(10)。將參數(shù)φ,μ,ε分別帶入式( 8 )即可得到當(dāng)前環(huán)境下，每類臨時限速出現(xiàn)的可能性，從而實現(xiàn)對臨時限速語義可信度的計算。

( 8 )

( 9 )

(10)

2.3 報文時效性需求

列控系統(tǒng)是典型的實時系統(tǒng)，需要在有效時間內(nèi)對報文做出實時響應(yīng)，因而報文與車載契約模型的事務(wù)特征之一是“時效性”，即在報文與車載雙向交互的仿真實驗中，車載提出對報文的需求，而報文需在有效時間tvalid內(nèi)給予反饋，且一旦超出tvalid，則說明報文錯誤或者丟失。舉例來說：當(dāng)列車準(zhǔn)備側(cè)線發(fā)車，且正線出站信號機(jī)旁設(shè)置了應(yīng)答器CZ時，應(yīng)答器Q接收到CTCS-1包后，車載發(fā)出對軌道區(qū)段長度NID_SIGNAL進(jìn)行驗證的請求，契約模型結(jié)合當(dāng)前運(yùn)行環(huán)境，約定只有當(dāng)該變量滿足NID_SIGNAL=0111 &T_SectionVerify

上述是以車載ATP計算控車曲線作為需求，分別從報文信息包語法模式、功能語義和時效性三方面提出了相應(yīng)的公理約束，如TelegramCover等，作為CPTA形式化建模和驗證的基礎(chǔ)。

3 基于CPTA實現(xiàn)車地契約關(guān)系的形式化建模與驗證

將報文語法、語義和時效性三部分約束作為系統(tǒng)狀態(tài)遷移的條件，不僅能夠?qū)崟r反映出報文與車載的交互狀態(tài)，且一旦出現(xiàn)報文信息包無法滿足車載的一致性需求時，還可以及時得到不一致發(fā)生的原因，以及對車載的影響。舉例來說，圖8為當(dāng)車載接收到CTCS-2包中的臨時限速后，在T11時間內(nèi)計算出當(dāng)前環(huán)境下限速值出現(xiàn)的可能性為0.9，因此列車會按照調(diào)度下發(fā)的該限速值安全行駛。下面就以臨時限速數(shù)據(jù)為例對報文-車載契約關(guān)系進(jìn)行建模。

圖8 基于CPTA的報文-車載契約模型圖形化描述示例

3.1 基于CPTA構(gòu)建報文-車載的契約模型

當(dāng)車載經(jīng)過應(yīng)答器接收到相應(yīng)的信息包后，會發(fā)出對報文驗證的請求，契約模型接收到該請求后，分別驗證報文的語法、語義和時效性，并將驗證結(jié)果同車載請求進(jìn)行一致性比對，若兩者一致，則代表該數(shù)據(jù)符合車載的安全性需求。圖9描述了車載ATP在計算MRSP曲線過程中對臨時限速的驗證過程，其中，圖9(a)表示車載ATP對臨時限速的驗證過程，圖9(b)表示契約模型驗證臨時限速可信度的過程。

圖9 基于CPTA驗證線路限速數(shù)據(jù)過程

當(dāng)ATP發(fā)出TSR_Check!請求后，契約模型調(diào)取TSR_ReliaJudge約束對臨時限速的可信度R進(jìn)行計算，然后向車載反饋TSRCorrect!命令。車載接收到TSRCorrect?命令后，根據(jù)數(shù)據(jù)的可信度執(zhí)行從狀態(tài)S_TSR到S_TSR_Receive的轉(zhuǎn)換。

本文提出的CPTA方法論旨在通過實時準(zhǔn)確地描述列車在不同運(yùn)行場景中與報文數(shù)據(jù)的交互過程，來定性分離環(huán)境中的耦合因素，并從語法、語義和時效三方面定量刻畫出其對報文的約束，將其映射為車載系統(tǒng)狀態(tài)遷移的條件，從而實現(xiàn)了車載解析并使用報文的可視化過程。

3.2 結(jié)果分析

為了證實CPTA契約模型驗證報文的有效性和實用性，本文基于上述報文數(shù)據(jù)約束規(guī)則和契約模型，在Visual Studio 2010環(huán)境中開發(fā)了基于CPTA契約模型的報文驗證軟件，并設(shè)計了兩組實驗，分別從報文驗證性能和效率兩方面，與以往報文室內(nèi)靜態(tài)仿真驗證和室外動態(tài)調(diào)試進(jìn)行對比。

實驗一選取某信號設(shè)備研發(fā)公司的20條C2線路原始報文作為報文驗證軟件的實驗數(shù)據(jù)，同時收集該線路以往室內(nèi)靜態(tài)驗證和室外動調(diào)過程中，由于報文失效造成的列車異常制動或降速次數(shù)，作為參考數(shù)據(jù)進(jìn)行對比。實驗二選擇復(fù)雜度遞增的3條C2線路作為實驗數(shù)據(jù)，對基于CPTA契約模型報文驗證、傳統(tǒng)室內(nèi)報文靜態(tài)驗證和室外動調(diào)三種方式的驗證時間進(jìn)行對比，且為了能夠合理表現(xiàn)室外動態(tài)調(diào)試時間，將實際動調(diào)時間縮小10倍，如圖10、圖11所示。

圖10 線路條數(shù)對列車異常制動次數(shù)的影響

圖10結(jié)果表明基于CPTA契約模型驗證報文幾乎能夠達(dá)到室外動態(tài)調(diào)試的效果，能夠識別傳統(tǒng)靜態(tài)報文仿真驗證無法識別的報文失效模式，如合包后軌道區(qū)段長度過長、應(yīng)答器JL信息不完備等。雖仍未能全面識別出所有的報文失效模式，但相比室內(nèi)報文驗證而言，已經(jīng)明顯提高了報文驗證的可靠性。圖11結(jié)果表明基于CPTA契約模型的報文驗證時間遠(yuǎn)小于動態(tài)調(diào)試時間，略大于室內(nèi)靜態(tài)報文仿真時間。隨著線路復(fù)雜度提升，驗證時間有所增加，但由于基于契約模型的報文驗證屬于線下驗證，這屬于可接受范圍，且從系統(tǒng)角度來看，該方法減少了整個列控系統(tǒng)調(diào)試和驗證時間。

圖11 線路復(fù)雜度對報文驗證所需時間的影響

4 結(jié)論

本文根據(jù)報文與車載間存在的契約關(guān)系，提出一種新的報文驗證方案，即通過構(gòu)建基于環(huán)境的概率時間自動機(jī)CPTA模型來形式化描述CTCS-2級車載ATP與報文間的交互過程，實現(xiàn)完備且有效的報文驗證。剖析了車載在不同運(yùn)行環(huán)境下使用報文生成動態(tài)監(jiān)控曲線的過程，并對該過程進(jìn)行FMEA分析，識別得到報文可能存在的失效模式。分別從語法、語義和時效性三方面提取ATP對報文的需求，作為CPTA模型中車載狀態(tài)遷移的條件，借助PVS定理證明工具證明了該契約模型的正確性。研究和實驗結(jié)果表明：

(1)基于報文-車載契約關(guān)系提取的報文數(shù)據(jù)語法約束能夠減少因數(shù)據(jù)范圍不足、合包距離過長或信息包變量描述不一致等造成的列車異常制動或降速的次數(shù)，且通過報文語義約束能夠及時發(fā)現(xiàn)TSR下發(fā)錯誤，并使列車導(dǎo)向安全側(cè)。

(2)基于CPTA契約模型的報文驗證能夠準(zhǔn)確、全面、高效地識別報文數(shù)據(jù)的失效模式，提高了報文數(shù)據(jù)的正確率，且縮短了整個列控系統(tǒng)測試和驗證時間。