周 果，趙會兵

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

安全分析是所有安全苛求系統(tǒng)開發(fā)的必要過程，是事前預示、控制風險和保障安全苛求系統(tǒng)安全性的有力手段。列控系統(tǒng)是典型的安全苛求系統(tǒng)，系統(tǒng)安全完整性等級要求為SIL4，隨機失效完整性應滿足標準中對SIL4等級的要求，即容許隱患率THR(Tolerant Hazard Rate)小于10-9/h[1]。對列控系統(tǒng)的安全分析包括定性安全分析和定量安全分析兩項任務，定性分析主要是全面地尋找導致隱患(Hazard)發(fā)生的原因，定量分析主要是計算隱患發(fā)生的可能性。對列控系統(tǒng)的定量分析是本文關注的核心問題，定量分析的結(jié)果一方面是判斷隱患控制措施有效性的標準，另一方面是幫助開發(fā)設計人員決策風險(Risk)可接受性的依據(jù)。

傳統(tǒng)定量安全分析方法(如故障樹分析(FTA)、故障模式影響和嚴重度分析(FMECA)、Markov鏈(MC))在對簡單小規(guī)模系統(tǒng)進行安全分析時有較好的效果，得益于它們易于學習和理解的優(yōu)點，自提出以來就被極大程度地推廣。然而隨著系統(tǒng)復雜度和規(guī)模的不斷提升，傳統(tǒng)安全分析方法已經(jīng)不能滿足基于計算機技術的列控系統(tǒng)安全分析的需求，依靠手工和單純?nèi)说穆?lián)想推理已不能得到可信的定量安全分析結(jié)果。例如FTA在描述系統(tǒng)失效行為的過程中，啟發(fā)式地聯(lián)想推理失效條件，形成邏輯門的輸入和輸出，在系統(tǒng)規(guī)模龐大或結(jié)構(gòu)復雜的情況下，不僅會遺漏失效事件之間的順序關系，也會遺漏某些可能的輸入輸出事件。FMECA在歸納遍歷所有組成器件失效模式和影響的過程中，需要安全工程師對系統(tǒng)行為非常熟悉，并對失效影響作出準確判斷，由于組成器件眾多，工作量巨大，難免會遺漏和出錯，最終導致定量分析結(jié)果不可信。MC方法在面對多對象并發(fā)系統(tǒng)建模時，手工獲得全局狀態(tài)和狀態(tài)遷移幾乎不可能，因此需要開發(fā)新的定量安全分析方法。

為了克服以上傳統(tǒng)安全分析方法的不足，學界提出了基于模型的安全分析(Model Based Safety Analysis)[2]，它是基于模型的系統(tǒng)工程(Model Based System Engineering)的重要組成部分，其核心意義在于讓設計工程師和安全工程師共同使用統(tǒng)一的系統(tǒng)行為模型，以系統(tǒng)設計的正常功能模型為基礎，使系統(tǒng)驗證和安全分析結(jié)合的更為緊密，得到完整可信的安全分析結(jié)果。2005年美國明尼蘇達大學JOSHI A等[2]首次提出基于Matlab/Simulink模型的安全分析方法。2007年BOZZANO M等[3]開發(fā)了基于故障注入和模型檢驗的安全分析工具NuSMV-SA/FSAP。2013年altarica3.0項目啟動，目的是開發(fā)基于失效邏輯建模語言Altarica的安全分析一體化平臺[4]。由于以上方法對模型行為信息的描述各有側(cè)重并不統(tǒng)一，且尚處于研究階段，本文結(jié)合基于模型安全分析的思想，應用Markov決策過程作為系統(tǒng)行為模型建?；A，以概率模型檢驗為安全分析基礎，提出了基于綜合行為模型CBM(Comprehensive Behaviour Model)的列控系統(tǒng)定量安全分析方法。

圖1 基于Markov決策過程的行為建模與定量安全分析過程

該方法分為兩個方面，綜合行為模型的模塊化建模和完整定量安全分析。圖1為該方法的任務剖面，以系統(tǒng)設計作為輸入開始，經(jīng)過建模和分析兩大過程最終輸出定量安全分析報告。

1 建模與定量安全分析基礎

1.1 基于模型的安全分析

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

1.2 Markov決策過程

由以上5方面的建模需求，選擇Markov決策過程MDP(Markov Decision Process)[5]作為建?；A，因其具有表達不確定行為和概率行為的雙重能力，又能實現(xiàn)物理行為、正常行為和失效行為的并發(fā)建模，是其他建模工具如Petri網(wǎng)、Markov鏈等不能比擬的。另外，由于建模過程中，每一時間步內(nèi)系統(tǒng)行為概率分布的確定并不依賴于之前歷史狀態(tài)的影響，只與當前狀態(tài)有關，符合無記憶即馬爾科夫性?；谝陨侠碛?，可以實現(xiàn)在統(tǒng)一的建?；A下完成CBM模型的建立。

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

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

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

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

n∈N

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

圖2 MDP的圖形表示

2 基于MDP的系統(tǒng)行為建模

2.1 基于MDP的物理行為建模

根據(jù)以上物理運動的設定，可建立列車物理運動的MDP模型，如圖3所示。對列車位置和速度的生成是迭代進行的，兩個物理量可選擇的動作集Act中僅有一個疊加動作，即圖3中的a1，表示同步地將下一時刻的速度增量Δv和位移增量Δl疊加到上一時刻的速度值v(t)和位移值l(t)上，得到下一時刻的速度值v(t+1)和位移值l(t+1)，表示規(guī)則如式( 1 )所示。每次疊加動作完全疊加到上一時刻的值之上，所以對速度和位移兩者單獨來講，動作a1以概率1到達下一狀態(tài)。

圖3 列車物理運動模型

( 1 )

2.2 基于MDP正常行為的建模

設列車制動觸發(fā)值與限速值的速度差為vc，當下一刻的車速v(t+1)使得命題brake：v(t+1)

圖4 列車正常行為模型

2.3 基于MDP的失效行為建模

失效行為是指對象內(nèi)部發(fā)生故障(Fault)后經(jīng)過演變，在對象邊界上使得表征功能的量產(chǎn)生錯誤(Error)，最終導致對象所要實現(xiàn)的某種功能喪失即失效(Failure)的一系列過程。一個對象的失效行為模型也是一個MDP，可能包含不確定行為和概率行為。失效行為的組成根據(jù)失效可恢復性分為瞬態(tài)性失效和永久性失效兩類。瞬態(tài)性失效指失效可在有限步時間內(nèi)恢復到正常狀態(tài)的失效模式，相反永久性失效指失效不能在有限步時間內(nèi)恢復到正常狀態(tài)的失效模式。根據(jù)失效觸發(fā)的形式，失效行為可分為時間性失效和請求性失效兩類。時間性失效指對象的失效過程是與時間相關的連續(xù)失效過程，而請求性失效指失效只在外界環(huán)境請求對象提供安全功能的時候發(fā)生。

這4種失效均可由MDP來進行建模。以列控系統(tǒng)中車載設備計算列車位置的安全功能為例，建立時間性瞬態(tài)失效模型；以RBC計算列車EoA為例，建立時間性永久失效模型；以車載設備與無線閉塞中心之間安全數(shù)據(jù)交互的安全功能為例，建立請求性瞬態(tài)失效模型；以列車請求制動的安全功能為例，建立請求性永久失效模型。4類失效行為的MDP模型如圖5所示。模型5(a)和5(b)分別是車載設備故障導致的列車定位錯誤和RBC計算EoA錯誤，狀態(tài)0和1分別表示未發(fā)生故障狀態(tài)和發(fā)生故障狀態(tài)；模型5(c)和5(d)分別表示車載設備與無線閉塞中心之間安全信息通信錯誤和車載設備請求制動失效，狀態(tài)0、1和2分別表示初始狀態(tài)、未發(fā)生故障狀態(tài)和發(fā)生故障狀態(tài)。請求性失效存在初始狀態(tài)是由于對請求的響應需要一個時間步長，為了使失效正好發(fā)生在安全功能被請求的時刻而沒有一個時間步長的延遲，增加了一個虛擬的初始請求，其觸發(fā)條件始終為真，這使得在下一次請求到來時，保證失效模型只對其做出一次響應。

圖5 4類失效行為模型

2.4 模塊化行為模型的綜合

根據(jù)以上3部分的建模方法和模型修訂規(guī)則，可建立列控系統(tǒng)中系統(tǒng)層面各實體的行為模型。為了得到完整統(tǒng)一的行為模型，需要將它們整合為綜合行為模型CBM(Comprehensive Behaviour Model)。根據(jù)并發(fā)系統(tǒng)建模理論[5]，定義兩個并發(fā)的MDP模型M1和M2，其合成的MDP模型為

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

使得

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

3 基于CBM模型的定量安全分析

3.1 定量安全分析

定量安全分析的目的是計算系統(tǒng)隱患發(fā)生的可能性即危險失效概率或危險失效率，并判斷它是否在可接受的概率風險范圍之內(nèi)。定量安全分析與定性安全分析相比，其優(yōu)勢在于它的值可作為設計人員比較和改進設計的參考指標，是設計人員按照定性安全分析結(jié)果對系統(tǒng)設計進行改進后的效果驗證。基于以上理由，本文采取的基于模型的定量安全分析必須保證足夠的正確性和完整性。正確性是指定量分析過程的確準確計算了導致隱患發(fā)生的一系列順序事件的可能性，而完整性是指所有導致隱患發(fā)生情形的可能性都被計算在定量分析過程中。

為了滿足正確性和完整性的要求，應用概率模型檢驗技術對CBM模型進行分析。概率模型檢驗技術確保對由CBM模型生成的狀態(tài)空間進行遍歷搜索，并對到達危險狀態(tài)的所有路徑的概率進行準確計算，同時現(xiàn)有的先進模型檢驗工具PRISM[6]可高效地處理大規(guī)模狀態(tài)空間分析，且PRISM語言可方便地描述包含不確定行為和概率行為的MDP模型。

定量安全分析包括兩類任務，基于系統(tǒng)正常行為的功能性驗證和基于CBM模型的危險失效概率計算。首先，即使正常行為的功能性驗證通過，證明了設計的安全功能可實現(xiàn)且危險狀態(tài)不可達，也不能證明在系統(tǒng)中某個失效或多個失效發(fā)生時系統(tǒng)仍然是安全的。其次，只要存在失效，隱患永遠不可避免會發(fā)生，定量分析的目的就是要確定各種失效情形出現(xiàn)的條件下，隱患發(fā)生的可能性被有效控制。因此，這兩類任務中前者是后者的基礎。

3.2 基于正常行為模型的驗證

3.3 基于CBM模型的危險失效概率計算

4 列控系統(tǒng)追蹤場景的定量安全分析

4.1 追蹤場景的CBM建模

為了驗證方法的有效性和先進性，選擇列控系統(tǒng)區(qū)間運行中的雙車追蹤場景為例進行定量安全分析，首先對系統(tǒng)進行CBM建模。如圖6所示，在CTCS3級列控系統(tǒng)中[8]，線路情況與第2章中相同，兩車初速度為12個速度單位，RBC將前車報告的位置信息和來自列控中心的軌道占用信息與聯(lián)鎖進路信息綜合為移動授權(quán)信息MA，將移動授權(quán)終點EoA發(fā)送給后車，后車根據(jù)EoA、自身當前位置po(t)、速度sp(t)、加速度ac(t)(包括減速度SB)、列車車長Length400 m、安全保護距離SafeDistance100 m和靜態(tài)限速Maxspeed等信息，計算當前限速速度sb和制動觸發(fā)速度bt，保證列車前端在危險點前停車，由于系統(tǒng)采用固定閉塞模式，即危險點在前車停車時所在區(qū)間之后整數(shù)個區(qū)間的入口處。當前車在300個長度單位位置處發(fā)生緊急情況制動停車時，后車對危險點進行追蹤，追蹤間隔一個閉塞區(qū)間。本文主要研究RBC和后車ATP之間協(xié)作產(chǎn)生的失效，故假設前車、地面軌道電路和應答器等設備正常。

圖6 CTCS3級雙車追蹤場景

本文采用PRISM工具對CBM模型進行建模和分析，PRISM工具[6]是由牛津大學開發(fā)的先進概率模型檢驗工具，PRISM語言是一種基于狀態(tài)的反應系統(tǒng)形式的建模語言，支持包括Markov決策過程MDP在內(nèi)的多種概率行為模型的建模和檢驗。語言遵循模塊化的建模思路，對組件模塊(Module)定義其局部狀態(tài)變量(Local Variable)或全局狀態(tài)變量(Global Variable)，多個模塊組合形成系統(tǒng)，系統(tǒng)全局狀態(tài)由各模塊的狀態(tài)組合確定。模塊的行為由一組命令(Command)組成，形式為

[]guard->prob_1：update_1+…+

prob_n：update_n

式中：標記[]中表示該命令的名稱用來控制命令的同步；guard為命令觸發(fā)的條件；prob_n為狀態(tài)轉(zhuǎn)移概率；update_n表示狀態(tài)更新。

圖7 EoA計算PRISM表達式

RBC計算好后車的EoA之后，通過狀態(tài)變量eoa_RTrain的更新將其發(fā)送給后車車載ATP，當eoa_RTrain的值在其初始值與設定線路長度Rail之間時，將值更新為下一時刻的eoa_RTrain值，供后車計算限速使用，其PRISM模型如圖8所示。命令標記“[t]”被添加到每條命令之前，模擬時鐘信息，使模型全局同步執(zhí)行可執(zhí)行的命令，eoa_RTrain′表示下一時刻的狀態(tài)值。

圖8 RBC控制發(fā)送EoA模型

自此，物理模型、正常行為和失效行為模型都已獲得，根據(jù)2.4節(jié)中CBM模型合成規(guī)則，將失效模型注入到物理模型和正常行為模型中，由于規(guī)則已經(jīng)詳細描述，這里不再重復。

4.2 追蹤場景的定量安全分析

本文使用對屬性規(guī)范語言概率計算樹邏輯PCTL的檢驗來實現(xiàn)第3章中定義的定量安全分析任務。使用G(global)模態(tài)邏輯操作符表達屬性，設ψ為MDP模型M上的一個路徑表達式，πi是無限路徑π的前綴，操作符G的定義為MMDP，πGψ??i≥0：MMDP，πiψ，表示對某條路徑來說所有狀態(tài)都使ψ成立。

第一步追蹤場景的功能性驗證，只需要證明后車的位置始終在EoA之前。由于物理行為和正常行為模型中沒有無限執(zhí)行路徑，且場景運行為一次性過程，因此無需對計算時間進行限制。通過PRISM計算屬性得到

Pmax=?[Gsafestop]=1

且Pmin=?[Gsafestop]=1

同時計算屬性得

Pmax=?[Gunsafestop]=0

且Pmin=?[Gunsafestop]=0

表達式

safestop=po_RTrain≤EoA_RTrain

unsafestop=safestop

計算結(jié)果表明功能性驗證滿足，物理行為與正常行為模型正確。圖9、圖10分別為兩車的位置和速度變化曲線，圖11為固定閉塞模式下后車EoA的變化曲線，與實際追蹤運行情況一致。

圖9 兩車位置變化曲線

圖10 兩車速度變化曲線

圖11 后車EoA變化曲線

第二步計算危險失效發(fā)生的概率，只需對綜合行為模型CBM進行定量概率可達性計算。假設場景中考慮的故障包括：ATP計算列車位置錯誤偏低，時間性瞬態(tài)失效概率為RTrainPoerror=7×10-9；ATP與RBC之間安全數(shù)據(jù)交互錯誤且被接受，請求性瞬態(tài)失效概率為RBCcomError=7×10-9；RBC計算列車EoA錯誤，時間性永久失效概率為RBCeoaError=7×10-9；ATP請求制動失效，請求性永久失效概率為RTrainBrError=7×10-9。

圖12、圖13中以RBC計算EoA錯誤為例，選擇了一條失效路徑。圖12顯示了兩列車的位置曲線，可見在11個時間單位處，RBC出現(xiàn)故障將錯誤的EoA值1 000發(fā)送給后車，使得后車不斷前行，在約38個時間單位、500個位置單位處與前車相撞。圖13中同時顯示了該失效路徑下兩車的速度曲線，可見前車制動后在30個時間單位時實現(xiàn)停車，但后車由于接收了EoA錯誤值，并未及時采取制動措施，而保持在13～14個速度單位之間持續(xù)運行。

圖12 RBC計算EoA錯誤使兩側(cè)相撞

圖13 RBC計算EoA錯誤使后車未制動

系統(tǒng)隱患是列車位置超過EoA點，即通過PRISM計算場景危險失效概率最大值Pmax=?[true∪unsafestop]=1.607 2×10-12，其中時態(tài)邏輯操作符∪的定義為MMDP，πψ1∪ψ2??i≥0：MMDP，πiψ2∧?j

本文使用PRISM4.2版本軟件，Intel CORE i5處理器，4G內(nèi)存計算機計算，MDP求解算法選擇值迭代算法，功能性驗證中生成狀態(tài)22 168個，概率遷移32 410個，不確定動作選擇32 410個，計算時間7.2 s，由于概率行為分布均為1，則概率遷移與不確定動作選擇數(shù)量相同。危險失效概率計算中，稀疏矩陣占用空間312 M，運行時間257 s，狀態(tài)空間5 597 187個，概率遷移25 195 039個，不確定動作選擇4 152 658個。

5 結(jié)論

本文提出了以Markov決策過程為基礎的列控系統(tǒng)行為模型的建模方法，通過該方法可對列控系統(tǒng)中的物理行為、正常行為和失效行為進行建模，并對其中的不確定行為和概率行為進行準確描述，最終經(jīng)過組合得到綜合行為模型CBM。提出了基于CBM模型的定量安全分析方法，克服了經(jīng)典方法中對離散事件模型危險失效概率計算在完整性和精確性上的不足，運用概率模型檢驗理論和工具，實現(xiàn)了危險失效概率的計算。以CTCS3級列控系統(tǒng)中的追蹤場景為例，證明了本方法的先進性和有效性，證明了該定量安全方法在系統(tǒng)級多實體交互安全分析中的適用性。

參考文獻：

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

[2]JOSHI A,MILLER S P,WHALEN M,et al.A Proposal for Model-based Safety Analysis[C]//Digital Avionics Systems Conference,2005.

[3]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.

[4] BATTEUX M,PROSVIRNOVA T,BRAMERET P A,et al.The Altarica 3.0 Project for Model-based Safety Assessment[C]//Industrial Informatics(INDIN),2013 11th IEEE International Conference on.New York:IEEE Press,2013:741-746.

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

[6]HINTON A,KWIATKOWSKA M,NORMAN G,et al.PRISM:A Tool for Automatic Verification of Probabilistic Systems[M].Tools and Algorithms for the Construction and Analysis of Systems,Berlin:Springer Berlin Heidelberg,2006:441-444.

[7]FOREJT V,KWIATKOWSKA M,NORMAN G,et al.Automated Verification Techniques for Probabilistic Systems[M].Formal Methods for Eternal Networked Software Systems,Berlin:Springer Berlin Heidelberg,2011:53-113.

[8]張曙光.CTCS-3 級列控系統(tǒng)總體技術方案[M].北京：中國鐵道出版社,2008.