盛紫琦+王曦+歐陽城添

摘要：鐵路車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)是一種典型的安全苛求系統(tǒng)，重點(diǎn)是保障系統(tǒng)運(yùn)營安全。對系統(tǒng)安全進(jìn)行了分析，建立UML場景時(shí)序圖，以此為基礎(chǔ)建立系統(tǒng)的標(biāo)號(hào)遷移模型，通過模型檢測對系統(tǒng)進(jìn)行安全性驗(yàn)證與分析，設(shè)計(jì)了系統(tǒng)的安全模型，為安全苛求系統(tǒng)的安全性分析與驗(yàn)證評(píng)估提供了一個(gè)完整的技術(shù)框架，具有理論及實(shí)際價(jià)值。

關(guān)鍵詞：安全性分析；形式化方法；模型檢測

中圖分類號(hào)：TP309

文獻(xiàn)標(biāo)識(shí)碼：A

文章編號(hào)：16727800（2017）004019103

0引言

鐵路車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)[1]屬于安全等級(jí)為SIL4的安全系統(tǒng)，是一種典型的安全苛求系統(tǒng)[2-3]。系統(tǒng)進(jìn)路子模塊擔(dān)負(fù)著確保行車安全的重要職責(zé)，各功能部件之間關(guān)系和控制邏輯十分復(fù)雜，不正確的聯(lián)鎖邏輯關(guān)系會(huì)導(dǎo)致列車相撞的災(zāi)難性事故，是安全要求最高的子模塊之一。 關(guān)于鐵路車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)安全性的研究較多，文獻(xiàn)[4]采用Event-B方法對道岔控制電路的安全規(guī)范進(jìn)行了形式化模型描述和驗(yàn)證分析，在系統(tǒng)開發(fā)早期及時(shí)發(fā)現(xiàn)設(shè)計(jì)錯(cuò)誤或漏洞；文獻(xiàn)[5]采用有色Petri 網(wǎng)對聯(lián)鎖進(jìn)路控制建立形式化分析模型，通過CPN Tools對模型的狀態(tài)空間進(jìn)行仿真分析，從而驗(yàn)證了系統(tǒng)形式化建模的正確性；文獻(xiàn)[6]以基本進(jìn)路為例，提出基于場景分析的系統(tǒng)形式化模型生成方法，該方法從安全質(zhì)量方面改善了安全苛求軟件的設(shè)計(jì)；文獻(xiàn)[7]采用Rhapsody工具對鐵路聯(lián)鎖系統(tǒng)的UML模型進(jìn)行功能模擬，根據(jù)模擬結(jié)果分析是否存在不安全進(jìn)路；文獻(xiàn)[8]通過基于進(jìn)程控制的EVALPSN程序模擬器對鐵路聯(lián)鎖系統(tǒng)安全性進(jìn)行模擬驗(yàn)證；文獻(xiàn)[9]利用Z語言對移動(dòng)閉塞情況下的聯(lián)鎖系統(tǒng)進(jìn)行形式化建模；文獻(xiàn)[10]采用VDM工具對丹麥鐵路聯(lián)鎖系統(tǒng)進(jìn)行形式化描述；文獻(xiàn)[12]采用符號(hào)化模型檢驗(yàn)策略和相應(yīng)軟件SMV對鐵路計(jì)算機(jī)聯(lián)鎖控制邏輯設(shè)計(jì)進(jìn)行形式化建模與驗(yàn)證。以上研究對鐵路車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)的形式化建模、安全性設(shè)計(jì)、功能模擬與仿真等具有較好的理論指導(dǎo)意義，但沒有從系統(tǒng)需求分析、形式化建模、安全分析到系統(tǒng)安全性設(shè)計(jì)模型方面提供完整的技術(shù)框架。 本文在前期研究成果[6， 13]基礎(chǔ)上，對鐵路車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)的進(jìn)路建立子模塊，建立系統(tǒng)安全性設(shè)計(jì)模型，為系統(tǒng)安全性分析與驗(yàn)證提供了一個(gè)完整的技術(shù)框架。

1鐵路車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)形式化建模

在鐵路車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)中，從車站值班人員開始辦理進(jìn)路到信號(hào)機(jī)開放，分為6個(gè)階段：①操作階段：值班人員按規(guī)定操作辦理進(jìn)路以確定進(jìn)路的范圍、方向、性質(zhì)（列車或調(diào)車）以及特征（基本進(jìn)路、變更進(jìn)路等）；②選路階段：根據(jù)已確定的進(jìn)路范圍，選出一條相應(yīng)的進(jìn)路；③道岔轉(zhuǎn)換階段：檢查已選出的道岔實(shí)際位置是否符合進(jìn)路要求，不相符時(shí)應(yīng)將其轉(zhuǎn)換到實(shí)際位置；④一致性檢查階段：檢查進(jìn)路中的各個(gè)道岔位置是否符合進(jìn)路要求，為鎖閉道岔作準(zhǔn)備；⑤進(jìn)路鎖閉階段：在道岔位置正確、進(jìn)路空閑、未建立敵對進(jìn)路的條件下，將道岔和進(jìn)路鎖閉，為信號(hào)開放作準(zhǔn)備；⑥開放信號(hào)階段：開放信號(hào)，允許列車或車列駛?cè)脒M(jìn)路。 采用UML時(shí)序圖描述列車進(jìn)路建立的場景如圖1所示。圖1中矩形框?yàn)榻换タ?，操作符par表示并發(fā)，操作符alt表示選擇，框中的虛線是分隔線，各消息含義如表1所示。

建立UML時(shí)序圖場景各部件對象，如User、ILController、Switch、Section、Signal的標(biāo)號(hào)遷移系統(tǒng)模型狀態(tài)及遷移關(guān)系描述如下，其中遷移條件stop表示暫時(shí)終止進(jìn)路建立，其余遷移條件具體含義見表1。

User=Q0， Q0=（routeSelect -> Q1）， Q1=（routeSetUpOK -> Q0|routeSetUpFailed -> Q2）， Q2=（stop -> Q0） ILController = Q0， Q0=（routeSelect -> Q1）， Q1=（conflictRouteCheck -> Q2 |routeCheck -> Q15 |switchCheck -> Q20）， Q2=（conflictRouteExisting -> Q3|noConflictRouteSetUp -> Q5）， Q3=（routeSetUpFailed -> Q4）， Q4=（stop -> Q0）， Q5=（switchCheck -> Q6）， Q6=（switchCorrect -> Q7），Q7=routeCheck -> Q8）， Q8=（routeEmpty -> Q9）， Q9=（switchLocked -> Q10）， Q10=（routeLock -> Q11）， Q11=（routeLocked -> Q12）， Q12=（signalClear -> Q13）， Q13=（signalCleared -> Q14）， Q14=（routeSetUpOK -> Q0）， Q15=（routeOcupied -> Q3 |routeEmpty -> Q16）， Q16=（switchCheck -> Q17）， Q17=（switchCorrect -> Q18）， Q18=（conflictRouteCheck -> Q19）， Q19=（noConflictRouteSetUp -> Q9）， Q20=（switchInCorect -> Q21|switchCorect -> Q23）Q21=（switchTransact -> Q22）， Q22=（switchTransactionErro -> Q3|switchCorrect -> Q23）Q23=（routeCheck -> Q24）， Q24=（routeEmpty -> Q25）， Q25=（conflictRouteCheck -> Q26）， Q26=（noConflictRouteSetUp -> Q9） Switch = Q0， Q0=（switchCheck -> Q1）， Q1=（switchInCorect -> Q2|switchCorect -> Q4）Q2=（switchTransact -> Q3）， Q3=（switchTransactionErro -> Q0|switchCorrect -> Q4）Q4=（switchLock -> Q5）， Q5=（switchLocked -> Q0） Section= Q0， Q0=（conflictRouteCheck->Q1|routeCheck -> Q4）， Q1=（conflictRouteExisting -> Q0 |noConflictRouteSetUp -> Q2）， Q2=（routeLock -> Q3）， Q3=（routeLocked -> Q0）， Q4=（routeOcupied -> Q0|routeEmpty -> Q5）， Q5=（conflictRouteCheck -> Q1） Signal = Q0， Q0=（signalClear -> Q1）， Q1=（signalCleared -> Q0）

在LTSA中執(zhí)行組合運(yùn)算后，得到系統(tǒng)的形式化模型如圖2所示，與圖2對應(yīng)狀態(tài)遷移關(guān)系的描述如下：

SysModel=Q0， Q0=（conflictRouteCheck->Q1|routeSelect->Q15）， Q1=（routeSelect->Q2）， Q2=（conflictRouteCheck -> Q3 |switchCheck -> Q10）， Q3=（conflictRouteExisting -> Q4 |noConflictRouteSetUp -> Q8）， Q4=（conflictRouteCheck -> Q5 |routeSetUpFailed -> Q7）， Q5=（routeSetUpFailed -> Q6）， Q6=（stop -> Q1）， Q7=（stop -> Q0 |conflictRouteCheck -> Q6）， Q8=（switchCheck -> Q9）， Q9= STOP， Q10=（switchInCorect -> Q11|switchCorect -> Q13）， Q11=（switchTransact -> Q12）， Q12=（switchTransactionErro->Q5 |switchCorrect -> Q13）， Q13=（switchLock -> Q14）， Q14= STOP， Q15=（conflictRouteCheck -> Q2 |conflictRouteCheck -> Q16|routeCheck -> Q17|switchCheck -> Q22）， Q16=（conflictRouteCheck -> Q3）， Q17=（routeOcupied -> Q4|routeEmpty -> Q18）， Q18=（conflictRouteCheck -> Q19|switchCheck -> Q21）， Q19=（switchCheck -> Q20）， Q20= STOP， Q21=（conflictRouteCheck -> Q20）， Q22=（conflictRouteCheck -> Q10|switchInCorect -> Q23|switchCorect-> Q25）， Q23=（conflictRouteCheck->Q11|switchTransact->Q24）， Q24=（switchTransactionErro -> Q4|conflictRouteCheck -> Q12|switchCorrect -> Q25）， Q25=（conflictRouteCheck -> Q13|switchLock -> Q26|routeCheck -> Q41）， Q26=（conflictRouteCheck -> Q14|routeCheck -> Q27）， Q27=（routeEmpty -> Q28）， Q28=（conflictRouteCheck->Q29|conflictRouteCheck->Q40）， Q29=（conflictRouteCheck->30）， Q30=（noConflictRouteSetUp->Q31）， Q31=（switchLocked-> Q32）， Q32=（routeLock -> Q33）， Q33=（routeLocked -> Q34）， Q34=（conflictRouteCheck -> Q35 |signalClear -> Q38）， Q35=（signalClear -> Q36）， Q36=（signalCleared ->Q37）， Q37=（routeSetUpOK->Q1）， Q38=（conflictRouteCheck->Q36|signalCleared->Q39）， Q39=（routeSetUpOK -> Q0|conflictRouteCheck -> Q37）， Q40=（conflictRouteCheck -> Q30）， Q41=（switchLock -> Q27|routeEmpty -> Q42）， Q42=（switchLock -> Q28|conflictRouteCheck -> Q43|conflictRouteCheck -> Q46）， Q43=（switchLock -> Q29|conflictRouteCheck -> Q44）， Q44=（switchLock -> Q30

從圖2可知，各部件的形式化模型在模型檢測工具LTSA中進(jìn)行組合運(yùn)算，沒有出現(xiàn)錯(cuò)誤標(biāo)志“-1”，說明系統(tǒng)在進(jìn)路建立過程中沒有出現(xiàn)各部件單元因競爭資源而造成循環(huán)等待的死鎖現(xiàn)象，系統(tǒng)功能正常。在LTSA中進(jìn)行功能模擬顯示，系統(tǒng)形式化模型能滿足功能需求。

2系統(tǒng)安全性驗(yàn)證

通過對需求場景功能危害分析，得到系統(tǒng)進(jìn)路基本安全需求模型如圖3所示，其可判定條件集F={{ routeSelect， switchInCorect， routeSetUpOK}，{ routeSelect， switchLockFailure， routeSetUpOK}， {routeSelect， conflictRouteExisting， routeSetUpOK}， {routeSelect， sectionOccupied， routeSetUpOK}，{routeSelect， conflictSignalClear， routeSetUpOK}}，模型中遷移條件sectionOccupied表示區(qū)段占用，conflictSignalClear表示敵對信號(hào)開放，switchLockFailure表示道岔鎖閉失效，其余遷移條件具體含義見表1。

圖3表明系統(tǒng)發(fā)出進(jìn)路預(yù)選命令后，不能在敵對進(jìn)路建立、道岔不在規(guī)定位置、道岔鎖閉失效、區(qū)段占用、敵對信號(hào)開放等情形下建立進(jìn)路。 在LTSA中將圖2所示系統(tǒng)形式化模型與圖3所示模型作同步積運(yùn)算，生成系統(tǒng)的同步積形式化模型，包含狀態(tài)結(jié)點(diǎn)數(shù)為119，遷移數(shù)為210，應(yīng)用前期研究成果“基于啟發(fā)式on-the-fly的擴(kuò)展TGBA模型檢測算法”[13]，對系統(tǒng)同步積形式化模型進(jìn)行安全性驗(yàn)證，檢測結(jié)果為“No，空的ETGBA”，檢測結(jié)點(diǎn)數(shù)為119，遷移數(shù)為210，所需時(shí)間為0.005 6秒，所需內(nèi)存空間為8 872KB。由于安全性驗(yàn)證結(jié)果為“No”， 該系統(tǒng)的同步積形式化模型為空，表明系統(tǒng)在通常功能場景下的控制邏輯滿足系統(tǒng)安全性要求，這一分析結(jié)果與當(dāng)前鐵路行業(yè)標(biāo)準(zhǔn)[14]中規(guī)定的基本聯(lián)鎖功能要求一致。

3結(jié)語

本文以鐵路車站計(jì)算機(jī)聯(lián)鎖系統(tǒng)安全性分析為研究實(shí)例，首先對系統(tǒng)的進(jìn)路建立子模塊進(jìn)行分析，建立半形式化描述的UML時(shí)序圖；然后根據(jù)UML時(shí)序圖進(jìn)行形式化建模，用標(biāo)號(hào)遷移系統(tǒng)模型對系統(tǒng)形式化建模進(jìn)行描述；最后通過對需求場景功能危害進(jìn)行分析，得出系統(tǒng)的基本安全屬性，并用代數(shù)模型描述系統(tǒng)的基本安全屬性，通過模型檢測技術(shù)對系統(tǒng)進(jìn)行安全性驗(yàn)證與分析，獲得安全性分析結(jié)果。判空檢測結(jié)果為空，證明本文建立的形式化模型是正確的，這一分析結(jié)果與當(dāng)前鐵路行業(yè)標(biāo)準(zhǔn)中規(guī)定的基本聯(lián)鎖功能要求相一致，驗(yàn)證了本文的一整套技術(shù)方法正確可行。 本文研究成果具有一定的理論價(jià)值和實(shí)踐意義，可為安全苛求軟件開發(fā)、安全性分析與驗(yàn)證、安全評(píng)估等提供有力的理論與技術(shù)支持，對于提高我國高速鐵路、國防武器裝備、航空航天等安全苛求領(lǐng)域的系統(tǒng)安全具有重要意義。

參考文獻(xiàn)：

[1]趙志熙.計(jì)算機(jī)聯(lián)鎖系統(tǒng)技術(shù)[M].北京：中國鐵道出版社，1999.

[2]S NEIL.Safety critical computer systems[M].Harlow，UK：AddisonWesley Longman.1996.

[3]酈萌，吳芳美.鐵路信號(hào)可靠性安全性理論及證實(shí)[M].北京：中國鐵道出版社，2008.

[4]張?jiān)?，王海?基于Event-B的計(jì)算機(jī)聯(lián)鎖安全規(guī)范描述與驗(yàn)證[J].計(jì)算機(jī)與通信信號(hào)，2013，12（11）：4749.

[5]陶玲， 宋軍.基于CPN的聯(lián)鎖進(jìn)路控制建模及驗(yàn)證[J].工業(yè)控制計(jì)算機(jī)，2014， 27（11）： 1216.

[6]王曦，徐中偉.基于場景分析的系統(tǒng)形式化模型生成方法[J].計(jì)算機(jī)科學(xué)，2012， 39（8）： 136140.

[7]Y M HON， M KOLLMANN.Simulation and verification of UMLbased railway interlocking designs[J].AvoCS，2006（6）：168172.

[8]K NAKAMATSU，Y KIUCHI，W Y CHEN，et al.Intelligent railway interlocking safety verification based on annotated logic program and its simulator[C].In： Proceedings of 2004 IEEE International Conference on Networking， Sensing and Control，Taipei， Taiwan： 2004： 694699.

[9]ABRIAL J R.Modeling in eventB：system and software engineering [M].Cambridge University Press，Cambridge，2010.

[10]P BEHM，M T OR.A successful application of B in a Large project[J].FM99Formal Methods，1999（6）：712722.

[11]熊振華，魏臻.基于UPPAAL的鐵路車站信號(hào)聯(lián)鎖系統(tǒng)模型驗(yàn)證[J].科學(xué)技術(shù)與工程，2008，8（7）：18431846.

[12]燕飛，唐濤.計(jì)算機(jī)聯(lián)鎖控制邏輯的模型檢驗(yàn)方法[J].鐵道通信信號(hào)，2009，45（5）：2629.

[13]王曦，徐中偉.基于啟發(fā)式onthefly的擴(kuò)展TGBA模型檢測算法[J].計(jì)算機(jī)學(xué)報(bào)， 2014，37（12）：25192529.

[14]中華人民共和國鐵道部.TB/T 30272002計(jì)算機(jī)聯(lián)鎖技術(shù)條件[M].北京： 中國鐵道出版社， 2002.（責(zé)任編輯：杜能鋼）