區間占用檢查邏輯的建模與安全分析

周 果,趙會兵

(北京交通大學 電子信息工程學院，北京 100044)

列車占用檢查一直以來主要依靠軌道電路來完成，但軌道電路在特殊環境下會出現故障。如天氣潮濕時發生“低道床”現象，使得軌道電路發生故障占用，在CTC中顯示為故障“紅光帶”；而當鋼軌表面生銹或列車較輕時，輪軌接觸電阻過大，使得軌道電路發生分路不良，在CTC中沒有顯示即發生故障“飛車”。以上兩種故障都不能真實反映區間中列車的占用情況，而傳統的列控中心設計中并沒有邏輯檢查功能，使得出現緊急情況時由調度員自行決策處理，帶來嚴重的安全隱患[1,2]。

以上問題的關鍵是CTC僅對區間軌道占用情況進行被動的顯示，對空閑、正常占用、故障占用和失去分路4種真實占用狀態無法區別所導致的，使得正常占用和故障占用都顯示為紅色，而空閑和失去分路都顯示為白色，由此也帶來了信號專業中“紅光帶”和“飛車”兩形象化術語的語義模糊問題，無法區分正常還是故障。解決列車占用檢查錯誤問題的關鍵是對不可信的軌道電路繼電器狀態信息進行預處理，以不同的顏色來顯示不同的邏輯占用狀態，設計區間占用邏輯檢查層，生成明確區分邏輯狀態的區間列車占用信息，提高CTC被動顯示的可信程度。列控中心軟件是典型的安全苛求軟件，需通過安全性分析證明其安全性要求滿足安全完整性等級SIL4[3]。然而傳統安全分析方法，如故障樹FTA和故障模式及影響分析FMEA，只適合靜態系統的分析，Markov鏈雖可對動態系統進行建模，但在系統規模大、交互復雜的情況下，人工的建模方式幾乎不可能遍歷所有狀態，Petri網方法可將系統狀態轉移的識別過程轉化為對系統并發行為的直接表達，但缺乏模塊化的建模規則，使得其分析能力受到限制。

為了克服以上傳統安全分析中遇到的困難，學界提出了基于模型的安全分析方法MBSA(Model Based Safety Analysis)，它是基于模型系統工程的重要組成部分，其核心理念是讓設計人員使用包括正常行為和故障行為兩者在內的系統行為模型進行安全分析。2005年JOSHI A等[4]首次提出了基于模型的安全分析方法，利用Simulink對飛機起落架制動系統進行了建模和分析。2007年BOZZANO M等[5]開發了基于故障注入和模型檢驗的安全分析平臺FSAP/NuSMV-SA，可對模型進行自動化分析，生成FTA和FMEA，并在2009年后研發了基于AADL擴展語言SLIM語言的自動化安全分析平臺COMPASS[6]。2012年LIPACZEWSKI A等[7]開發了SAML語言，可進行基于NuSMV和PRISM平臺的自動化安全分析。2013年至今達索航空等正在開發基于建模語言altarica3.0的自動化安全分析平臺OCAS[8]。

由于以上工具尚不成熟，還處于進一步研究階段。本文結合MBSA的思想，提出了基于Markov決策過程MDP的系統行為建模和分析方法，首次對列車占用檢查邏輯進行了安全分析和驗證，該方法綜合了以上MBSA方法的技術優點。如圖1所示：首先，對包括物理運動行為、正常行為和故障行為在內的3種行為分別進行建模，優點在于將系統中所有行為綜合統一到一個建模體系內；其次，對占用邏輯檢查層進行建模，處理來自軌道電路繼電器的設備狀態信息，并向CTC輸出安全的占用邏輯狀態，優點在于通過獨立模塊化降低了建模難度；第三，識別綜合行為模型CBM(Comprehensive Behavior Model)中的系統級目標功能和隱患，識別所有可能的故障模式的組合，對其進行基于概率計算樹邏輯PCTL的屬性表達，優點在于形式表達的準確無歧義；最后，運用形式驗證工具PRISM對隱患和故障模式進行模型檢驗，生成所有最小割集和危險失效概率，優點在于可高效地自動化計算。

圖1 建模與分析步驟

1 區間軌道行為建模

1.1 基于MDP的行為建模

對列控中心占用邏輯檢查軟件的分析需首先建立系統的行為模型，基于模型的安全分析方法，一方面強調系統建模，認為模型準確真實地反映系統抽象屬性是后續安全分析的基礎，直接關系安全分析結果的正確性；另一方面弱化分析過程，將分析過程交給自動化工具完成。要完整地描述系統的行為，需要包含以下5個方面的建模要求：首先是物理行為，指的是分析對象如列車在場景中實際運動的過程模型，是整個系統行為模型的基礎；其次是正常行為，指的是無故障前提下分析對象作為一個反應系統(Reactive System)對外界環境的響應控制邏輯；第三是故障行為，指的是分析對象中可能出現的故障模式對應的行為模型；第四是不確定(Non-deterministic)行為，指的是并發系統中下一步執行行為的選擇是不確定的；第五是概率(Probabilistic)行為，指的是一個行為的執行符合某種概率分布。將以上5種行為整合為一個行為模型稱為綜合行為模型CBM。

由于有以上5方面的建模需求，選擇Markov決策過程MDP(Markov Decision Process)[9]作為建模基礎，因為其具有表達不確定行為和概率行為的雙重能力，又能實現物理行為、正常行為和故障行為的并發建模，這是其他建模工具如Petri網、Markov鏈等難以比擬的。另外，由于建模過程中，下一時刻系統行為概率分布的確定并不依賴于之前的歷史狀態，而只與當前狀態有關，符合無記憶即馬爾科夫性。基于以上理由，可以實現在統一的建模基礎下完成CBM模型的建立。

給出Markov決策過程的形式定義。一個MDP是一個六元組。

M=(S,Act,P,s0,AP,L)

對于每個狀態s∈S，MDP在每一時刻至少選擇一項不確定性動作a∈Act，并按該動作的概率分布確定地執行。形式上每一步動作執行是一個有序對(ai,μi)，其中ai∈Act,μi∈P，i∈N。MDP中一條完整的路徑由一系列狀態與動作組成，設一條無限路徑為

式中：ai∈Act;μi∈P(〈si,ai+1,si+1〉)且μi>0,i≥0。設有限路徑為

它是無限路徑π的前綴，終止狀態為sn。對無線路徑或有限路徑ρ而言，它是第i個狀態si,記做π(i)或ρ(i)，跡記做tr(π)=(a0,μ0) (a1,μ1) (a2,μ2)…或tr(ρ)=(a0,μ0) (a1,μ1)(a2,μ2)…(an,μn)，由路徑上的所有動作組成。如圖2所示，圓表示狀態，三角形表示動作，虛線有向弧表示動作的選擇，實線有向弧表示概率狀態遷移，實線有向弧上的正實數表示動作的概率分布中該狀態遷移的概率，虛線有向弧上標注的是觸發該動作的條件衛士G，是由狀態變量組成的布爾表達式。

圖2 MDP的圖形表示

1.2 列車運動過程模型

本文設定列車通過區間場景如圖3所示，設定一條設計時速200 km/h以上的線路中，一段典型區間軌道區段共5段，從左至右依次為G1到G5，已知列車不減速通過該區間，列車前方無車占用，起始區段為G1，停止區段為G5，不存在斷鉤和改方情況，列車與后續列車處于同一信號許可內。在理想情況下，道床和軌道電路工作正常，當區段有車占用時，軌道電路繼電器觸點斷開，觸點狀態由TCC采集并發送給CTC，顯示為紅色；當區段無車占用時，軌道電路繼電器觸點閉合，在CTC顯示器上顯示為白色。

圖3 列車不減速通過區間場景

以上列車物理運動過程是一個MDP，如圖4所示。初始狀態0為模型初始狀態，目的是為了使狀態轉移的決策動作在狀態轉移條件滿足時執行，并與模型變遷編號一致，此時場景中無車。狀態1表示列車完全處于第一區段G1中，隨著列車的向前移動，所在位置按照表1中的狀態順序由狀態1至9依次變化，表中狀態標記“0”表示列車不處于該軌道區段，標記“1”則相反，定義變量t表示列車在各位置時的場景狀態變量。該模型中只存在動作move，表示列車向前運動，執行該動作條件衛士為true，表示列車運動無條件進行，該動作執行的概率分布為1，表示可準確地執行該動作。列車運動狀態轉移表見表1，g1～g5分別表示各區段的設備狀態。

圖4 列車物理運動過程MDP

tg1g2g3g4g5000000110000211000301000401100500100600110700010800011900001

1.3 正常行為模型

圖5 區段Gk正常行為模型

1.4 故障行為模型

故障行為是指對象內部發生故障(Fault)后經過演變，在對象邊界上使得表征功能的量產生錯誤(Error)，最終導致對象所要實現的某種功能喪失即失效(Failure)的一系列過程。一個對象的故障行為模型也是一個MDP，可能包含不確定行為和概率行為。根據故障觸發的形式，故障行為可分為時間性故障和請求性故障兩類。時間性故障指對象的故障過程是與時間相關的連續故障過程，而請求性故障指故障只在外界環境請求對象提供功能時發生。本文中故障占用和失去分路分別屬于時間性故障和請求性故障，且都是瞬態的，其MDP模型如圖6所示，其中的狀態0和1分別表示未發生故障狀態和發生故障狀態。請求性故障本應設置初始狀態，因為對請求的響應需要一個時間步長，可使故障正好發生在功能被請求的時刻而沒有一個時間步長的延遲，但本文中邏輯狀態的判決是在設備故障發生后進行的，不必同步，因此不必設置虛擬的初始狀態。

圖6 故障行為模型

2 邏輯檢查層設計與CBM建模

2.1 邏輯檢查層模型

在傳統TCC或CTC的設計中并沒有區間列車占用檢查邏輯判斷這一項安全功能，只是根據軌道電路繼電器狀態被動地進行傳輸和顯示該狀態，這導致在軌道電路出現故障時，TCC和CTC無法區分空閑、正常占用、故障占用和失去分路4種真實占用狀態，帶來嚴重安全隱患。為降低隱患風險，根據技術條件[10]對列控中心區間占用邏輯檢查功能進行改進，增加邏輯檢查層，對TCC采集而來的軌道電路繼電器狀態進行處理，再發送給CTC顯示終端，如圖7所示。邏輯檢查層將隱患風險較大的兩種設備狀態信息轉換為風險較低的4種邏輯狀態信息，并定義了相應的顯示顏色，對它們進行嚴格的區分，兩種設備狀態標記符號e和o的含義如圖7中紅色部分表示，4種邏輯狀態標記符號ne、no、fo和fe的含義如圖7中綠色部分表示。

圖7 邏輯檢查層

圖8 邏輯檢查層設計

邏輯檢查層是設備狀態信息與邏輯狀態之間的安全屏障，其狀態轉移規則如圖8所示，對第k個區段而言，其邏輯狀態的判決需要根據第k-1個區段和第k+1個區段的設備狀態和邏輯狀態的變化作為判決條件。圖8(a)表示設備狀態的轉移規則，其中標記o表示Gk設備狀態占用，e表示Gk設備狀態空閑，狀態轉移條件由設備狀態的出發標記和目的標記連接組成。圖8(b)表示邏輯狀態的轉移規則，狀態轉移條件由邏輯狀態的出發標記和目的標記連接組成。與文獻[10]中的技術要求和假設保持一致，其中實線轉移弧所帶的條件衛士是由Gk相鄰區段的設備狀態轉移事件和邏輯狀態轉移事件組成的布爾表達式，事件命名由出發標記到目的標記組合而成；虛線轉移弧①②屬于調整規則，分別與文獻[10]中6.1.11和6.1.12一致。邏輯檢查層模型是一個MDP，同樣可以1.1中的建模方式表達，這里不再贅述。

2.2 CBM行為模型的綜合

場景中各模型均是基于狀態和事件的模型，圖9為修正后Gk的正常行為模型。在考慮故障的情況下，正常狀態模型即為真實的設備狀態模型，其中增加了動作FE和FO，條件標記a～g表示觸發設備狀態轉移的條件衛士，是由列車運動狀態和故障狀態組合而成的布爾表達式。

圖9 修正后的正常行為模型

對邏輯檢查層模型的修正需要實現與設備狀態轉移的同步，邏輯狀態的轉移是由條件事件及它們的組合觸發的，但MDP是基于狀態的建模方法，不能直接表達事件。因此，本文提出了以標記n同步設備狀態層和邏輯檢查層的方法，并在邏輯檢查層模型中使用與設備狀態層相同的轉移條件，實現事件同步。定義Gk的邏輯狀態變量為lk，以邏輯狀態由正常占用狀態“1”到空閑“0”的判決為例，修正后的邏輯檢查層模型為

其中，lk=1∧lk+1=1表示Gk與Gk+1邏輯狀態為正常占用“1”時，Gk+1設備狀態滿足保持占用條件，Gk的邏輯狀態由正常占用變為空閑，此時Gk+1設備狀態的保持占用動作與Gk的狀態轉移動作同步完成。

根據物理行為模型、正常行為模型、故障行為模型和邏輯檢查層模型4部分的建模方法和模型修訂規則，可建立場景的行為模型即綜合行為模型CBM。根據并發系統建模理論[9]，定義兩個并發的MDP模型M1和M2，其合成的MDP模型為

M=M1‖M2=(S,Act,P,s0,AP,L)

使得

M=(S1×S2,Act1∪Act2,P,AP1∪AP2,L)

其中每一項的獲得可根據兩個MDP模型合成的規則迭代完成，這樣就得到了系統的綜合行為CBM模型，該模型將作為功能驗證和安全分析的輸入，進一步得到驗證和分析結果。

3 功能驗證與安全分析

3.1 功能驗證

本文采用由牛津大學開發的先進概率模型檢驗工具PRISM[11]對CBM模型進行建模和分析，支持包括MDP在內的多種概率行為模型的建模和檢驗。首先，建模過程經過驗證是正確的，即證明在無故障發生時，邏輯狀態能正確反映區間占用情況，且不會導致危險發生。對于一個模型MCBM，設定由故障狀態變量fek和fok組成故障模式集合F，如果計算樹邏輯CTL表達式

當CTC終端以2.1節中設計的四色來顯示占用邏輯狀態時，調度員可根據需要自行處理調度任務。考慮最不利情況，調度員在確認列車后方所有區段無車占用時，就有可能在該列車后方排入新的列車追蹤前車。因此場景中的隱患可表達為：場景中列車分路某一區段或跨越區段邊界時，被分路區段邏輯狀態處于空閑或故障占用狀態，且此時被分路區段后方所有區段均處于空閑或故障占用狀態。在PRISM中以l1～l5分別表示各區段的邏輯狀態模塊，以狀態值0～3分別表示邏輯狀態ne,no,fo和fe。該隱患可表示為

Hazardk=(t=k∨t=k+1)∧

(lk=0∨lk=2)∧(lk-1=0∨lk-1=2)∧

…∧(l1=0∨l1=2)

式中：t=k和t=k+1分別表示列車完全處于Gk或同時分路Gk+1兩類列車實際占用情況。

功能驗證的目的是證明占用檢查邏輯功能設計完整，即不考慮故障情況下，CTC可顯示區間中真實的列車占用情況。此時，割集為空即C=?，檢驗結果為false，即無故障發生時可安全地顯示占用情況，實際上此時邏輯狀態與設備狀態完全一致。

文獻[10]中附錄B.1涉及的故障占用判決以正常占用情形為例，PRISM生成的結果見表2，其中g1～g5分別表示各區段的設備狀態。以G3先發生故障占用為例，即fo3=1，G3邏輯狀態由故障占用變為空閑，此時G4設備狀態由空閑變占用，由于G3為故障占用，即邏輯狀態由空閑變為故障占用；然后G3設備狀態由占用變為空閑，邏輯狀態由故障占用變為空閑，此時G4設備狀態保持占用，即G4邏輯狀態由故障占用變為正常占用，與設計規范一致。

表2 附錄B.1路徑

3.2 危險情形安全分析

故障具有獨立并發性，當場景中軌道電路發生故障時，需找出所有可能導致隱患發生的故障組合即最小割集。此時，割集Cut≠?，對26個故障模式的組合進行檢驗，生成狀態572 285個，狀態轉移17 376 014個，模型生成時間1.039 s，屬性檢驗平均時間0.028 s，得到三階以內割集6個，最小割集2個，無單點故障，即邏輯檢查層可對任意的單一故障占用和失去分路故障進行防護，不會出現危險情況。列車完全處于單一區段Gk時,最小割集為C1={fok,fek,fok+1}和C2={fek-1,fok,fok+1}，處于跨壓相鄰兩區段Gk和Gk+1時,最小割集為C3={fek-1,fok,fok+1}和C4={fek,fok+1}。

C1以t=5為例檢驗完全處于G3時的危險，屬性檢驗結果為真，證例見表3。在t=4時滿足fe3=1且fo4=1的雙重故障情況，使得在t=5時l3=0，l2=2，l1=0，且列車邏輯占用完全處于G4，而此時列車應完全處于G3內，占用情形前移了一個區段，造成了危險，更重要的問題是由于G3發生瞬態故障占用在先，使得此時G2設備狀態為空閑，而邏輯狀態為故障占用，發生明顯的矛盾。因此，文獻[10]中限制條件7.2應進一步明確當列車由正常占用區段準備進入本區段時，本區段發生故障占用在先，下一區段故障占用在后，最終本區段失去分路的故障過程不適用。

表3 完全處于G3內時的危險

C2與C3包含元素相同，但導致的危險情況不同，以t=5和t=6為例檢驗完全處于G3及跨壓G3和G4時的危險。證例見表4，當t=5時，列車應完全處于G3內，而此時邏輯狀態顯示列車失去分路狀態完全處于G4內；當t=6時，列車應跨壓G3和G4，而此時邏輯狀態顯示列車以正常占用狀態完全處于G4內，兩種情形均帶來危險。這種故障過程沒有在限制條件中明確提出，應增加。

表4 完全處于G3或跨壓G3和G4時的危險

C4以t=6為例檢驗同時分路G3和G4時的危險，屬性的檢驗結果為真，證例見表5。在t=6時列車同時分路G3和G4，此時fe3=1即車尾所在G3處于失去分路狀態，使得l3=0即列車邏輯占用完全處于G4，占用情形前移了一個區段，造成了危險。因此，文獻[10]中限制條件7.3應進一步明確列車準備進入下一區段時，下一區段故障占用在先，本區段失去分路在后的故障過程不適用。

表5 跨壓G3和G4時G3的危險

3.3 危險失效概率計算

安全分析的最終任務是定量計算危險失效概率值，對MDP來說就是計算以初始狀態為起點的危險可達概率的最大值。

式中：Pmax=?為概率計算樹邏輯運算符，表示計算上限值。假設系統的失效概率密度函數符合指數分布f(t)=λe-λt(t≥0)，其中常數λ為指數分布失效率，若已知容許危險失效率λTHR，則可得[0,t]時間段內的累積容許危險失效概率為

根據廣鐵集團內部統計，高速線路區間軌道電路發生故障占用的概率為3.800×10-6，自動恢復正常的概率為0.1，列車通過時發生失去分路的概率為3.800×10-7，恢復正常的概率為0.6。以武廣高鐵為例，全長約1 100 km，計算得到場景危險失效概率返回值5.783×10-13，全程包含重復場景1 100/3個，即單程危險失效概率約為2.120×10-10，全程運行時間1 100/300 h，設定占用邏輯檢查功能單程容許危險失效率2.000×10-9/h，可得單程容許危險失效概率為7.339×10-9>2.120×10-10，所以危險失效概率風險在可接受范圍之內。

4 結論

通過在列控中心軟件中增加邏輯檢查功能對列車占用狀態進行處理，以四色顯示占用邏輯狀態，可保障區間行車的安全性。本文通過Markov決策過程方法建立列車通過區間場景的綜合行為模型CBM，準確地描述了區段占用設備狀態和邏輯狀態的判決關系，并驗證了CBM模型的完整性，分析了邏輯狀態判決設計的安全性，并找出了導致危險發生的準確故障組合情況，改進了技術條件中的限制條件表達，最后通過定量計算危險失效概率證明了設計的危險風險在可接受范圍之內。

參考文獻：

[1]陳鋼. 溫州動車追尾事故與 CTCS-2 技術規范中的安全隱患[J]. 軟件, 2012, 32(8): 27-30.

CHEN Gang. The Wenzhou Train Collision and the Safety Issue in CTCS-2 Specification[J].Software, 2012,32(8):27-30.

[2]李銘, 趙曄. 三點檢查邏輯對區間軌道電路分路不良的防護研究[J]. 鐵路通信信號工程技術, 2012, 9(3): 59-61.

LI Ming, ZHAO Ye. The Protection Research of Three Point Logic Checking for Block Track Circuit Fault Occupation Problem[J]. Railway Communication and Signaling Engineering Technology, 2012, 9(3): 59-61.

[3]British Standards Institution. EN50129 C Railway Applications-Communication, Signalling and Processing Systems-Safety Related Electronic Systems for Signalling[S]. United Kingdom:British Standards Institution, 2003.

[4]JOSHI A, MILLER S P, WHALEN M, et al. A Proposal for Model-based Safety Analysis[C]// Digital Avionics Systems Conference.New York: IEEE Press, 2005.

[5]BOZZANO M, VILLAFIORITA A. The FSAP/NuSMV-SA Safety Analysis Platform[J]. International Journal on Software Tools for Technology Transfer, 2007, 9(1): 5-24.

[6]BOZZANO M, CIMATTI A, KATOEN J P, et al. The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems[C]//Computer Safety,Reliability, and Security. Berlin:Springer Berlin Heidelberg, 2009: 173-186.

[7]LIPACZEWSKI M, STRUCK S, ORTMEIER F. SAML Goes Eclipse-Combining Model-based Safety Analysis and High-level Editor Support[C]// 2012 2nd Workshop on Developing Tools as Plug-ins (TOPI). New York: IEEE Press, 2012: 67-72.

[8]PROSVIRNOVA T, BRAMERET PA, RAUZY A. Model Based Safety Assessment: the AltaRica 3.0 Project[J]. Insight, 2013, 16(4):24-25.

[9]BAIER C, KATOEN J P. Principles of Model Checking[M]. Cambridge: MIT Press, 2008.

[10]中國鐵路總公司.運電高信函〔2014〕234號 中國鐵路總公司運輸局關于印發《列控中心區間占用邏輯檢查暫行技術條件》的通知[Z].2014.

[11]KWIATKOWSKA M, NORMAN G, PARKER D. PRISM: Probabilistic Model Checking for Performance and Reliability Analysis[J]. Acm Sigmetrics Performance Evaluation Review, 2009, 36(4):40-45.