鐵路計算機聯(lián)鎖系統(tǒng)安全關鍵軟件的安全性能建模方法

李　耀,張亞東,郭　進,晏　姍,饒　暢，曹雅鑫

(西南交通大學 信息科學與技術學院，四川 成都　610031)

鐵路信號是保障行車安全的重要基礎設備，許多鐵路信號系統(tǒng)軟件都是典型的安全關鍵軟件(Safety Critical Software)[1]，對安全性要求極為嚴格。安全性包括安全功能和安全性能兩個方面。安全功能主要指“系統(tǒng)滿足安全約束”及“構件或子系統(tǒng)失效對系統(tǒng)安全的影響”。安全性能包括安全完整度及風險等級等；安全完整度是指“系統(tǒng)在規(guī)定的條件下和規(guī)定的時間內完成安全功能的可能性”，風險等級是指“危害發(fā)生的概率及嚴重等級”[2-3]?，F(xiàn)有的形式化建模方法缺乏對系統(tǒng)狀態(tài)、行為及風險之間度量關系的描述，進行安全性分析時需要分別建立安全功能分析模型和安全性能分析模型，由于兩者使用的建模方法不同，容易出現(xiàn)模型表達不一致或彼此不理解對方模型的問題。

傳統(tǒng)的形式化方法，如自動機(Automata)，馬爾可夫決策過程(Markov Decision Processes，MDP)和馬爾可夫鏈(Markov Chain，MC)等，能夠為軟件設計提供統(tǒng)一的描述機制，但無法同時滿足安全功能及性能分析建模需求，且“平坦”的建模結構導致模型復雜。文獻[4]在有限確定的Automata的基礎上提出了概率自動機(Probabilistic Automata，PA)方法，用于描述系統(tǒng)的概率行為。文獻[5]在UML狀態(tài)圖(UML Statecharts)中引入概率特性，提出P-狀態(tài)圖(P-Statecharts)建模方法，支持不確定性分析，并具有層次性的優(yōu)點。文獻[6]針對系統(tǒng)概率不易確定的問題，提出確定性頻率有限自動機(Deterministic Frequency Finite Automata，DFFA)方法，并給出了轉化為確定性概率有限自動機(Deterministic Probabilistic Finite Automata，DPFA)算法，采用確定性的方式描述系統(tǒng)的度量關系。文獻[7]為Automata的狀態(tài)和變遷增加了“價格”特性，提出價格時間自動機(Priced Time Automata，PTA)方法，能夠反映系統(tǒng)響應過程中的消耗關系。文獻[8]針對鐵路信號系統(tǒng)提出一種關聯(lián)系統(tǒng)功能和風險等級的確定性的安全行為建模方法，反映了系統(tǒng)響應時風險等級的變化情況。PA，P-Statecharts和DFFA能夠描述鐵路信號系統(tǒng)安全完整度，PTA和安全行為方法能夠描述系統(tǒng)的風險等級，但PA，DFFA，PTA及安全行為方法均采用“平坦”的建模機制，不具有層次性，且不能同時滿足安全完整度和風險等級的建模需求；P-Statecharts受限于Statecharts語法，不能完全從根本上消除不確定性，且采用優(yōu)先級的機制導致模型復雜。同時，PA和P-Statecharts屬于不確定性的建模方法，與鐵路信號系統(tǒng)安全功能所要求的確定性存在分歧。

SyncCharts[9]是Charles André針對反應式系統(tǒng)提出的一種高效、清晰、確定的圖形化建模語言，具有層次性、并發(fā)性和優(yōu)先級搶占的特點，支持軟件安全功能分析建模，但不能進行定量計算，無法滿足鐵路信號系統(tǒng)安全關鍵軟件安全性能分析建模的需求。因此，本文在SyncCharts的狀態(tài)和變遷中增加轉移頻數(shù)和失效后果嚴重度2個參數(shù)，提出頻率風險SyncCharts建模方法和模型分析方法；以鐵路計算機聯(lián)鎖系統(tǒng)中的信號請求子系統(tǒng)為例，建立該子系統(tǒng)安全關鍵軟件安全性能分析模型，計算模型狀態(tài)的激活概率和風險等級，定量描述該子系統(tǒng)關鍵軟件的安全性能。

1　頻率風險SyncCharts建模方法

首先定義頻率風險SyncCharts的基本結構單元：頻率風險狀態(tài)轉移圖(DFRSTG)；然后在此基礎上給出頻率風險SyncCharts的定義、約束條件和宏步規(guī)則。

1.1　頻率風險SyncCharts定義

DFRSTG是一個具有唯一初始狀態(tài)、基于事件響應的狀態(tài)轉移圖。DFRSTG的狀態(tài)和變遷具有轉移頻數(shù)特性，表示保持原狀態(tài)和觸發(fā)變遷的次數(shù)。狀態(tài)具有失效后果嚴重度的特性，表示該狀態(tài)失效后導致的系統(tǒng)后果嚴重度的等級。變遷具有變遷類型屬性，類型集記為TTYPE::={TSTRONG,TWEAK,TSYNC}，其中TSTRONG為強變遷，TWEAK為弱變遷，TSYNC為同步變遷。

定義1 ：八元組(S,s0,Sf,G,T,f,a,r)稱為DFRSTG。其中：

S為有限狀態(tài)集；

s0∈S為缺省狀態(tài)；

Sf?S為終止狀態(tài)集；

G為可接受或產(chǎn)生的有限原子事件集；

T?S×α×TTYPE×TLABEL×S為變遷集；α∈N+為轉移優(yōu)先級；TLABEL::=G×G為變遷標號集，表示觸發(fā)變遷的事件和產(chǎn)生的動作；

f:S∪T→N+為頻數(shù)函數(shù)，給狀態(tài)和變遷分配頻數(shù)；

a:S→2A×G為狀態(tài)動作函數(shù)，其中A::={AENTER,AIN}，AENTER和AIN分別表示進入、處于狀態(tài)時需要產(chǎn)生的動作；

r:S→{CL1,CL2,CL3,CL4}為失效后果嚴重度的函數(shù)，用于給狀態(tài)分配失效后果嚴重度的等級，其中CL1，CL2，CL3，CL4分別表示可忽略的、容許的、不希望的和不容許的等級，且有CL4>CL3>CL2>CL1。

定義2： 四元組(S,stop,D,ρ)稱為頻率風險SyncCharts模型，記為DFRSC。其中：

stop∈S為根狀態(tài)，且sTYPE(stop)=SMACRO；

D為DFRSC包含的有限DFRSTG集；

ρ:S→2D為DFRSTG分配函數(shù)，且?s∈S·ifsTYPE(s)=SBASICthenρ(s)=? elseρ(s)≠?。

根據(jù)定義2，DFRSC的層次結構是以stop為根，以SMACRO狀態(tài)為中間節(jié)點，以SBASIC狀態(tài)為葉子節(jié)點的1個層次樹。

DFRSTG中，變遷t∈T的源狀態(tài)記為σ(t)， 目標狀態(tài)記為τ(t)。 對任意SMACRO狀態(tài)s2，s2包含的頻率風險狀態(tài)轉移圖dFRSTG∈D，有?s1∈dFRSTG.S，稱s1為s2的孩子，簡記為s1∈ρ(s2)；稱s2是s1的雙親，記為s2=η(s1)。ρ(s)的自反傳遞閉包ρ*(s)::=ρ(s)∪∪{s1:ρ*(s)·ρ*(s1)}表示s的孩子集合。DFRSTG的狀態(tài)有多條變遷時，每條變遷的優(yōu)先級不同，且強變遷的優(yōu)先級最高，同步變遷的優(yōu)先級最低。

DFRSC的層次性使得DFRSC所有狀態(tài)均為stop的孩子狀態(tài)，且狀態(tài)的父子關系不存在循環(huán)，變遷不能跨越狀態(tài)層次；TSYNC變遷的源狀態(tài)為SMACRO狀態(tài)，且包含的DFRSTG均有至少1個終止狀態(tài)，具體滿足以下約束：

(1)?s:Sstop·s∈ρ*(stop)；

(2)?s,s1,s2:S·ifs1=η(s),s2=η(s)，thens1=s2；

(3)?s:S,s?ρ*(s)；

(4)?t:T·η(σ(t))=η(τ(t))；

(5)?t:T·ift.TTYPE=TSYNCthen

sTYPE(σ(t))=SMACRO∧?dFRSTG:DFRSTG∈ρ(σ(t))·dFRSTG.Sf≠?∧ ?t1:T·ift1≠t,σ(t1)=σ(t) thent1.TTYPE≠TSYNC。

1.2　DFRSC宏步規(guī)則

DFRSC從1組格局轉移到下一組格局的過程稱為1個宏步。宏步反映了DFRSC對事件的計算過程。

格局為DFRSC的1組穩(wěn)定狀態(tài)集，DFRSC的格局集合記為o(DFRSC)。初始格局表示DFRSC默認狀態(tài)集，記為o0(DFRSC)。 對DFRSC的任意一組格局u∈o(DFRSC)，stop∈u； 同時?s:S∈u·ifstype(s)=SMACROthen ?dFRSTG:DFRSTG∈ρ(s)， ?1s1∈dFRSTG.S·s1∈u。

SyncCharts中，狀態(tài)及其所有出發(fā)變遷構成反應細胞。DFRSC在SyncCharts反應細胞的基礎上增加了轉移頻數(shù)和失效后果嚴重度這2個參數(shù)，但不改變SyncCharts的確定性原則，轉移過程滿足SyncCharts的宏步規(guī)則[9]，即DFRSC在當前格局下，以反應細胞為核心，根據(jù)細胞的層次結構、反應細胞變遷類型及優(yōu)先級，依照SyncCharts宏步規(guī)則計算下一組穩(wěn)定狀態(tài)。

由于DFRSC的層次性，同一組格局激活不同層次上的反應細胞，將導致格局轉移到不同的穩(wěn)定狀態(tài)。宏步規(guī)則中未被激活的反應細胞稱之為休眠細胞EDRC，激活的反應細胞稱之為激勵細胞ERRC，其中保持原狀態(tài)的激勵細胞記為EHRC，觸發(fā)變遷的細胞記為ETRC。DFRSTG的1組格局u滿足u=EHRC.s∪ETRC.s∪EDRC.s，且EHRC.s∩ETRC.s=?，ERRC.s∩EDRC.s=?。

2　DFRSC模型分析

MDP[10]是描述系統(tǒng)隨機性和不確定性的基本結構之一，具有成熟的模型分析方法[11]。將DFRSC轉化為等價的MDP，再通過MDP的模型分析方法實現(xiàn)DFRSC的模型分析。

定義3：DFRSC的格局序列hu=u0,u1,u2,u3，…稱為DFRSC的路徑，記為h(DFRSC)。且有

(1)u0=o0(DFRSC)；

(2) ?i>0,ui+1∈n(ui)。

n(ui)為格局u的可達格局集合。DFRSC路徑為DFRSC從初始格局開始可能的執(zhí)行過程的格局序列。

定義4： 四元組(S,s0,p,w)稱為MDP模型，記為DMDP。其中有

w:S→N+為成本函數(shù)。

定義5：DMDP上的1個狀態(tài)序列hs=s0,s1,s2,s3，…稱為DMDP的路徑，記為h(DMDP)，且?i>0，p(si+1|si)>0。

S′=o(DFRSC)；

p′=S′×S′→R，如果：

(1)?s1,s2∈S′·ifp′(s2|s1)>0，?u1,u2∈o(DFRSC)， thens1=u1，s2=u2，u2∈n(u1)，p′(s2|s1)=p′(u2|u1)；

(2)?u1,u2∈o(DFRSC)，ifu2∈n(u1)，then ?s1,s2∈S′,s1=u1,s2=u2，p′(s2|s1)>0，p′(s2|s1)=p′(u2|u1)；

w′:S′→N+，且?s1∈S′·?1u1∈o(DFRSC)·s1=u1,w′(s1)=r(u1)。

m(DFRSC)定義了DFRSC向DMDP結構的轉移關系，表明DFRSC的格局集和DMDP結構的狀態(tài)集有相同的狀態(tài)空間。T和p分別描述了DFRSC和DMDP的轉移關系，表明DFRSC和DMDP具有相同的執(zhí)行路徑。

定理2： 設Ψ是DFRSC的路徑u0,u1,u2，…向DMDP路徑s0,s1,s2,…的映射，則?hs∈h(m(DFRSC))??hu∈h(DFRSC):Ψ(hu)=hs。

證明：根據(jù)定理1，m(DFRSC)將DFRSC映射為DMDP，DFRSC的格局集對應DMDP的狀態(tài)集。?s1,s2∈S，如果p(s2|s1)>0，則DFRSC中?u1,u2∈o(DFRSC)，u1=s1，u2=s2，u2∈n(u1)。故MDP的任意路徑hs=s0,s1,s2，…均對應DFRSC的1條格局路徑hu=u0,u1,u2，…。

假設?hu∈h(DFRSC)，Ψ(hu)=hs， 但s′?h(m(DFRSC))。 根據(jù)定理1有：hu=u0,u1,…,ui,ui+1，…，且?i,ui+1≠n(ui)， 否則hs∈h(m(DFRSC))。 但如果存在此(ui,ui+1)， 則hu?h(DFRSC)。 故DFRSC中的任意路徑hu=u0,u1,u2，…對應DMDP的1條路徑hs=s0,s1,s2，…。

定理2表明DFRSC和DMDP結構同構，有相同的狀態(tài)序列和轉移關系，如圖1所示。

圖1　DFRSC與DMDP算法同構示意圖

DFRSC轉換為DMDP的算法原理為：將DFRSC的格局轉換為DMDP結構的狀態(tài)；計算DFRSC格局的最大失效后果嚴重度，將該嚴重度轉化為DMDP對應狀態(tài)的成本；將DFRSC的頻數(shù)轉化為DMDP的概率。該算法如圖2所示。圖2中：f(ei.s)為反應細胞ei狀態(tài)的頻數(shù)；f(ei.t)為變遷t的頻數(shù)。

采用PRISM[12]模型分析工具對DMDP模型進行分析，得到DMDP的轉移概率和即時期望成本；這2個量就是DFRSC模型的激活概率和風險等級；用這2個量則可以定量描述鐵路信號子系統(tǒng)安全關鍵軟件的安全性能。

3　計算機聯(lián)鎖系統(tǒng)的DFRSC建模

3.1　信號請求子系統(tǒng)的DFRSC模型

鐵路計算機聯(lián)鎖系統(tǒng)是一個對安全功能和性能要求嚴格的系統(tǒng)。以計算機聯(lián)鎖系統(tǒng)[13]的信號請求子系統(tǒng)為例建立DFRSC模型，通過DFRSC模型定量分析信號請求子系統(tǒng)各個狀態(tài)的轉移頻率，識別系統(tǒng)的風險等級。信號請求子系統(tǒng)的工作流程為：信號請求子系統(tǒng)接收到信號請求時，檢查道岔是否選排一致；若沒有選排一致，則轉換道岔使道岔到其需求位置，若轉換道岔失敗，則放棄信號請求；若選排一致或道岔轉換到需求位置后，如果進路內首區(qū)段空閑，或首區(qū)段故障但開放引導信號，則信號請求成功，廣播安全請求消息給其他子系統(tǒng)[14]。在計算過程中，如果DSignal模型接收到取消信號，則模型立即重置；若通信中斷，則DSignal模型進入安全防護狀態(tài)。該系統(tǒng)涉及8個事件，事件名稱及其含義見表1。

圖2　DFRSC轉換為DMDP算法

事件含義事件含義g1信號請求　　g2道岔選排一致g3道岔轉換超時g4首區(qū)段空閑　g5引導信號　　g6取消信號　　g7通信中斷　　g8安全信號請求

信號請求子系統(tǒng)的DFRSC模型如圖3所示。在圖3中，IN:g8表示處于該狀態(tài)時廣播消息g8；s1(CL3/50)表示r(s1)=CL3，f(s1)=50； 50/g1表示轉移頻數(shù)為50，轉移條件為g1發(fā)生；變遷①表示變遷的優(yōu)先級為1；狀態(tài)s0，s1，s2，s3，s4，s5，s6，s7分別表示選排判斷、等待信號請求、接受信號請求、道岔選排不一致、道岔選排一致、正常安全信號請求、首區(qū)段故障下安全信號請求和通信中斷后的故障狀態(tài)。

圖3　信號請求子系統(tǒng)的DFRSC模型

根據(jù)定義2，信號請求子系統(tǒng)DFRSC模型的定義如下。

DSignal=(S,stop,D,ρ)，其中：

S={DSignal,s0,s1,s2,s3,s4,s5,s6,s7}；

stop={DSignal}；

D={s8,s9}；

ρ(DSignal)={s8},ρ(s0)={s9}；

s8=((s0,s7),s0,?,(g6,g7),((t1:s0,1,

TSTRONG,(g6,?),s0),(t2:s7,1,

TSTRONG,(notg7,?),s0),(t3:s0,2,

TSTRONG,(g7,?),s7)),f(s0)=100,

f(s7)=1,f(t1)=2,f(t2)=2,f(t3)=

3,a(s0)=a(s7)=?,r(s0)=CL3,

r(s7)=CL4)；

s9=((s1,s2,s3,s4,s5),s1,?,(g1,g3,g4,g5,g8),((t1:s1,1,TSTRONG,((g1,?),s2),(t2:s2,1,TSTRONG,((notg2,?),s3),(t3:s3,2,TSTRONG,(notg3,?),s1),(t4:s2,2,TSTRONG,(g2,?),s4),(t5:s3,1,TSTRONG,(g3,?),s4),(t6:s4,1,TSTRONG,(g4,?),s5),(t7:s4,2,TSTRONG,(notg3andg5,?),s6),f(t1)=50,f(t2)=10,f(t3)=1,f(t4)=40,f(t5)=9,f(t6)=46,f(t7)=3,f(s1)=50,f(s5)=46,f(s6)=3,f(s2)=f(s3)=f(s4)=0,a(s1)=a(s2)=a(s3)=a(s4)=?,a(s5)=a(s6)=(IN,g8),r(s1)=r(s2)=r(s3)=r(s4)=CL3,r(s5)=r(s6)=CL4)。

3.2　Signal模型分析

圖4　Signal模型的DMDP模型

利用PRISM[14]對圖4所示的DMDP模型進行分析。利用PRISM的實驗機制，分析狀態(tài)s0，s1，s2，s3，s4，s5，s6，s7在DMDP的10個執(zhí)行周期中的激活概率，如圖5所示。由圖5可知：狀態(tài)s2，s4，s5的激活概率較大，表明信號請求子系統(tǒng)經(jīng)常運行在接收信號請求、道岔選排一致、滿足安全條件這3個狀態(tài)，因此為降低信號請求子系統(tǒng)的可容忍危害概率，保證子系統(tǒng)的安全性能，在對信號請求子系統(tǒng)進行設計和測試時需要對這3個狀態(tài)進行重點分析。選取DMDP執(zhí)行第1～10個執(zhí)行周期，分析信號請求子系統(tǒng)在10個執(zhí)行周期中的風險等級變化情況，如圖6所示。由圖6可知：在8個執(zhí)行周期后，風險等級逐步穩(wěn)定在3.8。根據(jù)EN50128[15]的風險管理可知，信號請求子系統(tǒng)的風險等級較高，因此應采取相關技術措施對該子系統(tǒng)進行風險控制和管理，保證子系統(tǒng)的風險等級滿足安全性能的要求。

圖5　Signal狀態(tài)激活概率與執(zhí)行周期的關系

圖6　Signal風險等級與執(zhí)行周期的關系

由此可見，采用頻率風險SyncCharts模型和模型分析方法，對信號請求子系統(tǒng)安全關鍵軟件的安全性能進行分析，可以辨識出子系統(tǒng)經(jīng)常運行的狀態(tài)和風險等級，從而指導軟件系統(tǒng)的優(yōu)化設計、重點測試和維護，為系統(tǒng)的風險控制和管理提供定量參考，保障軟件滿足安全性能的要求。

4　結　語

本文通過在SyncCharts建模方法中增加轉移頻數(shù)和失效后果嚴重度2個參數(shù)，提出1種鐵路信號安全關鍵軟件安全性能建模的頻率風險SyncCharts方法，給出了頻率風險SyncCharts的定義、約束條件和宏步規(guī)則；為對頻率風險SyncCharts進行模型分析，給出了將頻率風險SyncCharts轉化為MDP的算法，通過對MDP模型進行分析，實現(xiàn)對頻率風險SyncCharts模型的分析。以鐵路計算機聯(lián)鎖系統(tǒng)中信號請求子系統(tǒng)安全關鍵軟件為例，分析得到鐵路信號子系統(tǒng)的激活概率和風險等級2個安全性能指標，定量描述該子系統(tǒng)關鍵軟件的安全性能，為軟件的優(yōu)化設計、重點測試和維護提供定量參考，從而為系統(tǒng)的風險控制和管理提供定量參考，保障軟件滿足安全性能要求。本文提出的方法已在CBTC聯(lián)鎖系統(tǒng)軟件設計及開發(fā)中得到應用，實踐表明該方法對信號子系統(tǒng)安全關鍵軟件安全性能的設計、測試和風險管理具有一定的指導意義。

[1]DAVID L Parnas，A John van Schouwen，SHU PO Kwan. Evaluation of Safety-Critical Software[J]. Communications of the ACM, 1990, 33(6):636-648.

[2]CENLEC.EN50126 Railway Applications—the Specification and Demonstration of Reliability，Availability，Maintainability and Safety(RAMS) [S].Geneva：International Electrotechnical Commission，2002.

[3]白鑫, 王陽, 郭湛. 基于EN50126標準的鐵路聯(lián)調聯(lián)試安全分析[J]. 中國鐵道科學, 2011, 32(4):104-108.

(BAI Xin，WANG Yang，GUO Zhan.Safety Analysis on System Integration Test and Commissioning for Railway Based on EN50126 Standard[J]. China Railway Science, 2011, 32(4):104-108. in Chinese)

[4]MICHAEL O RABIN. Probabilistic Automata [J]. Information and Control, 1963, 6(3): 230-245.

[5]DAVID N Jansen，HOLGER Hermanns，JOOST-PIETER Katoen. A Probabilistic Extension of UML Statecharts[C]//Formal Techniques in Real-Time and Fault-Tolerant Systems. London: Springer Berlin Heidelberg, 2002: 355-374.

[6]COLIN de la Higuera. Grammatical Inference: Learning Automata and Grammars [M].New York: Cambridge University Press, 2010: 329-353.

[7]GERD Behrmann，KIM G Larsen，JACOB I Rasmussen. Priced Timed Automata: Algorithms and Applications[C]//Formal Methods for Components and Objects. Leiden: Springer Berlin Heidelberg, 2005: 162-182.

[8]喻鋼, 劉曉文, 熊靜, 等. 高速鐵路列控中心軟件安全性需求形式化建模[J]. 鐵道學報, 2013, 35(7): 74-79.

(YU Gang，LIU Xiaowen，XIONG Jing，et al. Formalized Modeling of Safety Requirements of High-Speed Train Control Center Software System[J]. Journal of the China Railway Society, 2013, 35(7): 74-79. in Chinese)

[9]CHARLES André.Semantics of SyncCharts[M].Nice: University of Nice Sophia Antipolis，2003: 1-76.

[10]TOMAS Brazdil，KRISHNENDU Chatterjee，MARTIN Chmelik，et al. Verification of Markov Decision Processes Using Learning Algorithms[J]. Computer Science, 2015, 8837:98-114.

[11]CHRISTEL Baier, JOOST Pieter Katoen. Principles of Model Checking[M]. Massachusetts: The MIT Press, 2008: 832-899.

[12]MARTA Kwiatkowska，GETHIN Norman，DAVID Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach[J]. International Journal on Software Tools for Technology Transfer, 2004, 6(2):128-142.

[13]楊揚, 潘明, 何梅芳. 聯(lián)鎖軟件的Petri網(wǎng)形式化定義[J]. 中國鐵道科學, 2002, 23(3):49-54.

(YANG Yang，PAN Ming，HE Meifang. Formal Specification of the Interlocking Software Using Petri Nets[J]. China Railway Science, 2002, 23(3):49-54. in Chinese)

[14]楊淘. 基于CBTC系統(tǒng)的聯(lián)鎖邏輯研究[D]. 成都：西南交通大學，2014.

(YANG Tao. The CBTC Based Interlocking Logic Research [J]. Chengdu：Southwest Jiaotong University，2014. in Chinese)

[15]BSI Standards Publicaiton. BS EN 50128:2011 Railway Applications-Communication，Signaling and Processing Systems-Software for Railway Control and Protection Systems [S].Geneva：International Electrotechnical Commission, 2011.