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

周 果,趙會(huì)兵

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

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

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

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

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

圖1 建模與分析步驟

1 區(qū)間軌道行為建模

1.1 基于MDP的行為建模

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

由于有以上5方面的建模需求，選擇Markov決策過程MDP(Markov Decision Process)[9]作為建?；A(chǔ)，因?yàn)槠渚哂斜磉_(dá)不確定行為和概率行為的雙重能力，又能實(shí)現(xiàn)物理行為、正常行為和故障行為的并發(fā)建模，這是其他建模工具如Petri網(wǎng)、Markov鏈等難以比擬的。另外，由于建模過程中，下一時(shí)刻系統(tǒng)行為概率分布的確定并不依賴于之前的歷史狀態(tài)，而只與當(dāng)前狀態(tài)有關(guān)，符合無記憶即馬爾科夫性。基于以上理由，可以實(shí)現(xiàn)在統(tǒng)一的建?；A(chǔ)下完成CBM模型的建立。

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

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

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

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

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

圖2 MDP的圖形表示

1.2 列車運(yùn)動(dòng)過程模型

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

圖3 列車不減速通過區(qū)間場(chǎng)景

以上列車物理運(yùn)動(dòng)過程是一個(gè)MDP，如圖4所示。初始狀態(tài)0為模型初始狀態(tài)，目的是為了使?fàn)顟B(tài)轉(zhuǎn)移的決策動(dòng)作在狀態(tài)轉(zhuǎn)移條件滿足時(shí)執(zhí)行，并與模型變遷編號(hào)一致，此時(shí)場(chǎng)景中無車。狀態(tài)1表示列車完全處于第一區(qū)段G1中，隨著列車的向前移動(dòng)，所在位置按照表1中的狀態(tài)順序由狀態(tài)1至9依次變化，表中狀態(tài)標(biāo)記“0”表示列車不處于該軌道區(qū)段，標(biāo)記“1”則相反，定義變量t表示列車在各位置時(shí)的場(chǎng)景狀態(tài)變量。該模型中只存在動(dòng)作move，表示列車向前運(yùn)動(dòng)，執(zhí)行該動(dòng)作條件衛(wèi)士為true，表示列車運(yùn)動(dòng)無條件進(jìn)行，該動(dòng)作執(zhí)行的概率分布為1，表示可準(zhǔn)確地執(zhí)行該動(dòng)作。列車運(yùn)動(dòng)狀態(tài)轉(zhuǎn)移表見表1，g1～g5分別表示各區(qū)段的設(shè)備狀態(tài)。

圖4 列車物理運(yùn)動(dòng)過程MDP

tg1g2g3g4g5000000110000211000301000401100500100600110700010800011900001

1.3 正常行為模型

圖5 區(qū)段Gk正常行為模型

1.4 故障行為模型

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

圖6 故障行為模型

2 邏輯檢查層設(shè)計(jì)與CBM建模

2.1 邏輯檢查層模型

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

圖7 邏輯檢查層

圖8 邏輯檢查層設(shè)計(jì)

邏輯檢查層是設(shè)備狀態(tài)信息與邏輯狀態(tài)之間的安全屏障，其狀態(tài)轉(zhuǎn)移規(guī)則如圖8所示，對(duì)第k個(gè)區(qū)段而言，其邏輯狀態(tài)的判決需要根據(jù)第k-1個(gè)區(qū)段和第k+1個(gè)區(qū)段的設(shè)備狀態(tài)和邏輯狀態(tài)的變化作為判決條件。圖8(a)表示設(shè)備狀態(tài)的轉(zhuǎn)移規(guī)則，其中標(biāo)記o表示Gk設(shè)備狀態(tài)占用，e表示Gk設(shè)備狀態(tài)空閑，狀態(tài)轉(zhuǎn)移條件由設(shè)備狀態(tài)的出發(fā)標(biāo)記和目的標(biāo)記連接組成。圖8(b)表示邏輯狀態(tài)的轉(zhuǎn)移規(guī)則，狀態(tài)轉(zhuǎn)移條件由邏輯狀態(tài)的出發(fā)標(biāo)記和目的標(biāo)記連接組成。與文獻(xiàn)[10]中的技術(shù)要求和假設(shè)保持一致，其中實(shí)線轉(zhuǎn)移弧所帶的條件衛(wèi)士是由Gk相鄰區(qū)段的設(shè)備狀態(tài)轉(zhuǎn)移事件和邏輯狀態(tài)轉(zhuǎn)移事件組成的布爾表達(dá)式，事件命名由出發(fā)標(biāo)記到目的標(biāo)記組合而成；虛線轉(zhuǎn)移?、佗趯儆谡{(diào)整規(guī)則，分別與文獻(xiàn)[10]中6.1.11和6.1.12一致。邏輯檢查層模型是一個(gè)MDP，同樣可以1.1中的建模方式表達(dá)，這里不再贅述。

2.2 CBM行為模型的綜合

場(chǎng)景中各模型均是基于狀態(tài)和事件的模型，圖9為修正后Gk的正常行為模型。在考慮故障的情況下，正常狀態(tài)模型即為真實(shí)的設(shè)備狀態(tài)模型，其中增加了動(dòng)作FE和FO，條件標(biāo)記a～g表示觸發(fā)設(shè)備狀態(tài)轉(zhuǎn)移的條件衛(wèi)士，是由列車運(yùn)動(dòng)狀態(tài)和故障狀態(tài)組合而成的布爾表達(dá)式。

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

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

其中，lk=1∧lk+1=1表示Gk與Gk+1邏輯狀態(tài)為正常占用“1”時(shí)，Gk+1設(shè)備狀態(tài)滿足保持占用條件，Gk的邏輯狀態(tài)由正常占用變?yōu)榭臻e，此時(shí)Gk+1設(shè)備狀態(tài)的保持占用動(dòng)作與Gk的狀態(tài)轉(zhuǎn)移動(dòng)作同步完成。

根據(jù)物理行為模型、正常行為模型、故障行為模型和邏輯檢查層模型4部分的建模方法和模型修訂規(guī)則，可建立場(chǎng)景的行為模型即綜合行為模型CBM。根據(jù)并發(fā)系統(tǒng)建模理論[9]，定義兩個(gè)并發(fā)的MDP模型M1和M2，其合成的MDP模型為

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

使得

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

其中每一項(xiàng)的獲得可根據(jù)兩個(gè)MDP模型合成的規(guī)則迭代完成，這樣就得到了系統(tǒng)的綜合行為CBM模型，該模型將作為功能驗(yàn)證和安全分析的輸入，進(jìn)一步得到驗(yàn)證和分析結(jié)果。

3 功能驗(yàn)證與安全分析

3.1 功能驗(yàn)證

本文采用由牛津大學(xué)開發(fā)的先進(jìn)概率模型檢驗(yàn)工具PRISM[11]對(duì)CBM模型進(jìn)行建模和分析，支持包括MDP在內(nèi)的多種概率行為模型的建模和檢驗(yàn)。首先，建模過程經(jīng)過驗(yàn)證是正確的，即證明在無故障發(fā)生時(shí)，邏輯狀態(tài)能正確反映區(qū)間占用情況，且不會(huì)導(dǎo)致危險(xiǎn)發(fā)生。對(duì)于一個(gè)模型MCBM，設(shè)定由故障狀態(tài)變量fek和fok組成故障模式集合F，如果計(jì)算樹邏輯CTL表達(dá)式

當(dāng)CTC終端以2.1節(jié)中設(shè)計(jì)的四色來顯示占用邏輯狀態(tài)時(shí)，調(diào)度員可根據(jù)需要自行處理調(diào)度任務(wù)?？紤]最不利情況，調(diào)度員在確認(rèn)列車后方所有區(qū)段無車占用時(shí)，就有可能在該列車后方排入新的列車追蹤前車。因此場(chǎng)景中的隱患可表達(dá)為：場(chǎng)景中列車分路某一區(qū)段或跨越區(qū)段邊界時(shí)，被分路區(qū)段邏輯狀態(tài)處于空閑或故障占用狀態(tài)，且此時(shí)被分路區(qū)段后方所有區(qū)段均處于空閑或故障占用狀態(tài)。在PRISM中以l1～l5分別表示各區(qū)段的邏輯狀態(tài)模塊，以狀態(tài)值0～3分別表示邏輯狀態(tài)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或同時(shí)分路Gk+1兩類列車實(shí)際占用情況。

功能驗(yàn)證的目的是證明占用檢查邏輯功能設(shè)計(jì)完整，即不考慮故障情況下，CTC可顯示區(qū)間中真實(shí)的列車占用情況。此時(shí)，割集為空即C=?，檢驗(yàn)結(jié)果為false，即無故障發(fā)生時(shí)可安全地顯示占用情況，實(shí)際上此時(shí)邏輯狀態(tài)與設(shè)備狀態(tài)完全一致。

文獻(xiàn)[10]中附錄B.1涉及的故障占用判決以正常占用情形為例，PRISM生成的結(jié)果見表2，其中g(shù)1～g5分別表示各區(qū)段的設(shè)備狀態(tài)。以G3先發(fā)生故障占用為例，即fo3=1，G3邏輯狀態(tài)由故障占用變?yōu)榭臻e，此時(shí)G4設(shè)備狀態(tài)由空閑變占用，由于G3為故障占用，即邏輯狀態(tài)由空閑變?yōu)楣收险加?；然后G3設(shè)備狀態(tài)由占用變?yōu)榭臻e，邏輯狀態(tài)由故障占用變?yōu)榭臻e，此時(shí)G4設(shè)備狀態(tài)保持占用，即G4邏輯狀態(tài)由故障占用變?yōu)檎Ｕ加?，與設(shè)計(jì)規(guī)范一致。

表2 附錄B.1路徑

3.2 危險(xiǎn)情形安全分析

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

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

表3 完全處于G3內(nèi)時(shí)的危險(xiǎn)

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

表4 完全處于G3或跨壓G3和G4時(shí)的危險(xiǎn)

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

表5 跨壓G3和G4時(shí)G3的危險(xiǎn)

3.3 危險(xiǎn)失效概率計(jì)算

安全分析的最終任務(wù)是定量計(jì)算危險(xiǎn)失效概率值，對(duì)MDP來說就是計(jì)算以初始狀態(tài)為起點(diǎn)的危險(xiǎn)可達(dá)概率的最大值。

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

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

4 結(jié)論

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

參考文獻(xiàn)：

[1]陳鋼. 溫州動(dòng)車追尾事故與 CTCS-2 技術(shù)規(guī)范中的安全隱患[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]李銘, 趙曄. 三點(diǎn)檢查邏輯對(duì)區(qū)間軌道電路分路不良的防護(hù)研究[J]. 鐵路通信信號(hào)工程技術(shù), 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]中國鐵路總公司.運(yùn)電高信函〔2014〕234號(hào) 中國鐵路總公司運(yùn)輸局關(guān)于印發(fā)《列控中心區(qū)間占用邏輯檢查暫行技術(shù)條件》的通知[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.