鐵路車站計算機聯鎖系統安全性分析

盛紫琦+王曦+歐陽城添

摘要：鐵路車站計算機聯鎖系統是一種典型的安全苛求系統，重點是保障系統運營安全。對系統安全進行了分析，建立UML場景時序圖，以此為基礎建立系統的標號遷移模型，通過模型檢測對系統進行安全性驗證與分析，設計了系統的安全模型，為安全苛求系統的安全性分析與驗證評估提供了一個完整的技術框架，具有理論及實際價值。

關鍵詞：安全性分析；形式化方法；模型檢測

中圖分類號：TP309

文獻標識碼：A

文章編號：16727800（2017）004019103

0引言

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

1鐵路車站計算機聯鎖系統形式化建模

在鐵路車站計算機聯鎖系統中，從車站值班人員開始辦理進路到信號機開放，分為6個階段：①操作階段：值班人員按規定操作辦理進路以確定進路的范圍、方向、性質（列車或調車）以及特征（基本進路、變更進路等）；②選路階段：根據已確定的進路范圍，選出一條相應的進路；③道岔轉換階段：檢查已選出的道岔實際位置是否符合進路要求，不相符時應將其轉換到實際位置；④一致性檢查階段：檢查進路中的各個道岔位置是否符合進路要求，為鎖閉道岔作準備；⑤進路鎖閉階段：在道岔位置正確、進路空閑、未建立敵對進路的條件下，將道岔和進路鎖閉，為信號開放作準備；⑥開放信號階段：開放信號，允許列車或車列駛入進路。 采用UML時序圖描述列車進路建立的場景如圖1所示。圖1中矩形框為交互框，操作符par表示并發，操作符alt表示選擇，框中的虛線是分隔線，各消息含義如表1所示。

建立UML時序圖場景各部件對象，如User、ILController、Switch、Section、Signal的標號遷移系統模型狀態及遷移關系描述如下，其中遷移條件stop表示暫時終止進路建立，其余遷移條件具體含義見表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中執行組合運算后，得到系統的形式化模型如圖2所示，與圖2對應狀態遷移關系的描述如下：

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中進行組合運算，沒有出現錯誤標志“-1”，說明系統在進路建立過程中沒有出現各部件單元因競爭資源而造成循環等待的死鎖現象，系統功能正常。在LTSA中進行功能模擬顯示，系統形式化模型能滿足功能需求。

2系統安全性驗證

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

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

3結語

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

參考文獻：

[1]趙志熙.計算機聯鎖系統技術[M].北京：中國鐵道出版社，1999.

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

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

[4]張越，王海峰.基于Event-B的計算機聯鎖安全規范描述與驗證[J].計算機與通信信號，2013，12（11）：4749.

[5]陶玲， 宋軍.基于CPN的聯鎖進路控制建模及驗證[J].工業控制計算機，2014， 27（11）： 1216.

[6]王曦，徐中偉.基于場景分析的系統形式化模型生成方法[J].計算機科學，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的鐵路車站信號聯鎖系統模型驗證[J].科學技術與工程，2008，8（7）：18431846.

[12]燕飛，唐濤.計算機聯鎖控制邏輯的模型檢驗方法[J].鐵道通信信號，2009，45（5）：2629.

[13]王曦，徐中偉.基于啟發式onthefly的擴展TGBA模型檢測算法[J].計算機學報， 2014，37（12）：25192529.

[14]中華人民共和國鐵道部.TB/T 30272002計算機聯鎖技術條件[M].北京： 中國鐵道出版社， 2002.（責任編輯：杜能鋼）