形式化的安全分析方法在智能軌道交通的應用

劉莎晨，韓 濤，朱天民，李思遠

（卡斯柯信號有限公司北京分公司，北京 100160）

1 概述

形式化方法基于數學基礎，可運用計算機的工具進行檢查和分析驗證[1]。鐵路行業的安全相關標準EN50129也推薦了形式化方法，“系統安全完整性等級SIL為SIL3或SIL4時，推薦采用形式化方法對系統設計和開發一致性進行校驗”[2]。

全自動駕駛（Fully Automatic Operation，FAO）系統作為智能軌道交通的必然發展趨勢，近年來得到了廣泛關注。FAO通過自動控制系統代替列車駕駛員、調度員執行的工作，減少了人為失誤對系統安全運行的影響。針對FAO系統這種功能復雜、組件交互頻繁、交互信息量大、時序特征復雜的系統，對其采用形式化的安全分析方法也勢在必行。卡斯柯作為軌道交通信號行業的先進技術企業，自主研發了國產化的TRANAVI列車運行控制系統。為保障系統的“自主可控，安全可信”，卡斯柯也致力于形式化方法的研究，包括形式化方法建模、驗證以及測試等多方面的研究，并運用于在安全保障領域。

在軌道交通領域，國內外學者也對系統安全分析方法進行了研究，驗證了STAMP及STPA用于鐵路安全分析的可行性[3]。文獻[4]從系統論的角度分析了甬溫線高鐵事故，不僅考慮了設備故障和人為失誤，還考慮了整個社會技術系統。此外，應用STPA對CBTC系統進行了分析，以識別事故場景，但對控制器內部算法沒有展開說明。John Thomas[5]提出了不安全的控制行為的生成算法，該算法基于過程模型中的系統變量，自動生成不適當的控制行為。文獻[6]以CTCS-1級列控系統RDC為研究對象，結合了STPA的安全分析與UPPAAL的建模和校驗，對安全分析的結果進行了驗證。

目前安全分析和形式化方法的結合在智能軌道交通領域的應用較少，針對以上現實背景以及面臨的挑戰，結合形式化方法和安全分析的STAMP理論，本文以FAO車載ATP為研究對象，按照STPA的步驟進行安全分析。

2 STPA概述

2004年，麻省理工學院的Nancy Leveson首先提出了基于系統理論的STAMP[7]模型。STAMP將安全定義為一個控制問題，認為導致事故的原因是控制不足或與安全相關的約束執行不力，而非組件的故障或失效。基于STAMP模型，Leveson提出了用于危險致因分析的STPA方法。

STPA的分析步驟如圖1所示。

圖1 STPA的步驟

3 應用實例：基于STPA與形式化結合的車載ATP分析方法

3.1 步驟一：定義系統級危害及安全約束

車載設備ATP根據速度-距離模式曲線監控列車運行，為避免列車運行時與其他列車相撞，對應的安全需求為在列車運行時，車載設備要確保列車與前車保持安全距離。事故，危害及安全約束如表1所示。

3.2 步驟二：建立控制結構

本文選擇車載ATP作為控制器，列車接口單元TIU作為執行器，車載ATP通過TIU輸出接口向列車輸出制動指令。車載ATP通過SDU獲取列車速度信息，通過BTM接收應答器的信息，獲取列車位置信息。通過TIU輸入接口獲取列車制動的反饋信息。

利用XSTAMPP工具，建立列車緊急制動和緩解的控制過程的控制結構模型，如圖2所示。

3.3 步驟三：識別不安全的控制行為

根據STPA方法論中提供的四種引導詞，結合控制結構的控制行為。利用XSTAMP進行UCA的識別。UCA如表2所示。

使用XSTAMPP工具，可以選擇生成上下文表，從而得到車載設備的系統行為規則，如圖3所示。

安全需求轉換為中文描述如下：

SR1：當車載ATP處于SM模式（列車ATP防護下的駕駛模式）時，速度超過允許速度（緊急制動干預速度），速度誤差小于規定值，ATP應施加緊急制動。

SR2：當車載ATP處于SM模式時，列車越過行車許可終點時，ATP應施加緊急制動。

SR3：當車載ATP處于SM模式時，速傳輸入的速度差值超過規定值，ATP應該施加緊急制動。

表1 事故、危害及安全約束

圖2 車載ATP控制結構

表2 不安全的控制行為

圖3 車載ATP行為規則

圖4 致因場景

圖5 LTL形式化規范

SR4：當車載處于RM模式（限制人工駕駛模式），速度超過允許速度（固定限制速度如20km/h），速度誤差小于規定值，ATP應施加緊急制動。

SR5：車載ATP輸出緊急制動后，當列車速度大于0，不能緩解緊急制動。

SR6：車載ATP輸出緊急制動后，當列車速度未知時，不能緩解緊急制動。

3.4 步驟四：識別致因場景

根據系統的功能處理過程，以及STPA方法論中所定義的分析引導圖。識別列車制動未實施的原因以及安全需求。

通過XSTAMPP工具自動將危險控制措施轉換為線性時間邏輯LTL的形式化語句，可用于日后的驗證活動。如圖5所示。

例如：SSR1.30 的 LTL 表達式為（（（（（Mode==SM）&&（SDU SpeedGappermitspeed）））→（（controlAction==Emergencybrake））））該表達式意為：當列車處于SM模式時，速度超過允許速度（緊急制動干預速度），速度誤差小于規定值，ATP應施加緊急制動。與需求SR1相一致。

4 結論與未來工作

本文將基于STPA的方法與形式化方法進行結合，利用形式化的分析工具來輔助STPA的分析過程。本文完成的工作如下：（1）從系統層面，找出了車載ATP對列車控制過程中的危險，同時確定了相應的安全約束。（2）建立了車載系統的控制結構，并根據四種引導詞，分析得到其不安全控制行為。（3）建立了包含過程模型的車載ATP的控制結構。（4）致因場景分析，即通過遍歷控制回路，找出可能導致不安全控制行為的原因。（5）通過XSTAMPP軟件工具來輔助分析過程，使得分析更加準確和完整，最終細化的安全需求包含自然語言描述和LTL形式化語言的表述。

隨著大數據、云計算、物聯網等先進技術的發展，智能軌道交通，從傳統的信號系統，逐漸走向軌道交通的互聯化、網絡化。比如隨著5G（第5代移動通信）技術的發展，在下一代的基于車車通信的列控系統中，可以進一步縮短列車運行間隔，甚至實現列車的近距離的同步運行，即虛擬編組。由此可能給列車運行安全帶來新的挑戰。STPA是基于系統理論的安全分析方法，還有XSTAMPP等軟件輔助分析過程，對于復雜系統的功能安全分析更具優勢。而形式化方法采用嚴謹的手段，邏輯精確，無二義性。因此在接下來的工作中，進一步探索STPA的應用范圍，研究STPA方法與形式化驗證相結合的分析方法，能更好的保障智能軌道交通的安全，提升系統性能。