形式化的安全分析方法在智能軌道交通的應(yīng)用

劉莎晨，韓 濤，朱天民，李思遠(yuǎn)

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

1 概述

形式化方法基于數(shù)學(xué)基礎(chǔ)，可運(yùn)用計(jì)算機(jī)的工具進(jìn)行檢查和分析驗(yàn)證[1]。鐵路行業(yè)的安全相關(guān)標(biāo)準(zhǔn)EN50129也推薦了形式化方法，“系統(tǒng)安全完整性等級SIL為SIL3或SIL4時，推薦采用形式化方法對系統(tǒng)設(shè)計(jì)和開發(fā)一致性進(jìn)行校驗(yàn)”[2]。

全自動駕駛（Fully Automatic Operation，F(xiàn)AO）系統(tǒng)作為智能軌道交通的必然發(fā)展趨勢，近年來得到了廣泛關(guān)注。FAO通過自動控制系統(tǒng)代替列車駕駛員、調(diào)度員執(zhí)行的工作，減少了人為失誤對系統(tǒng)安全運(yùn)行的影響。針對FAO系統(tǒng)這種功能復(fù)雜、組件交互頻繁、交互信息量大、時序特征復(fù)雜的系統(tǒng)，對其采用形式化的安全分析方法也勢在必行?？ㄋ箍伦鳛檐壍澜煌ㄐ盘栃袠I(yè)的先進(jìn)技術(shù)企業(yè)，自主研發(fā)了國產(chǎn)化的TRANAVI列車運(yùn)行控制系統(tǒng)。為保障系統(tǒng)的“自主可控，安全可信”，卡斯柯也致力于形式化方法的研究，包括形式化方法建模、驗(yàn)證以及測試等多方面的研究，并運(yùn)用于在安全保障領(lǐng)域。

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

目前安全分析和形式化方法的結(jié)合在智能軌道交通領(lǐng)域的應(yīng)用較少，針對以上現(xiàn)實(shí)背景以及面臨的挑戰(zhàn)，結(jié)合形式化方法和安全分析的STAMP理論，本文以FAO車載ATP為研究對象，按照STPA的步驟進(jìn)行安全分析。

2 STPA概述

2004年，麻省理工學(xué)院的Nancy Leveson首先提出了基于系統(tǒng)理論的STAMP[7]模型。STAMP將安全定義為一個控制問題，認(rèn)為導(dǎo)致事故的原因是控制不足或與安全相關(guān)的約束執(zhí)行不力，而非組件的故障或失效?；赟TAMP模型，Leveson提出了用于危險(xiǎn)致因分析的STPA方法。

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

圖1 STPA的步驟

3 應(yīng)用實(shí)例：基于STPA與形式化結(jié)合的車載ATP分析方法

3.1 步驟一：定義系統(tǒng)級危害及安全約束

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

3.2 步驟二：建立控制結(jié)構(gòu)

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

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

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

根據(jù)STPA方法論中提供的四種引導(dǎo)詞，結(jié)合控制結(jié)構(gòu)的控制行為。利用XSTAMP進(jìn)行UCA的識別。UCA如表2所示。

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

安全需求轉(zhuǎn)換為中文描述如下：

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

SR2：當(dāng)車載ATP處于SM模式時，列車越過行車許可終點(diǎn)時，ATP應(yīng)施加緊急制動。

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

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

圖2 車載ATP控制結(jié)構(gòu)

表2 不安全的控制行為

圖3 車載ATP行為規(guī)則

圖4 致因場景

圖5 LTL形式化規(guī)范

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

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

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

3.4 步驟四：識別致因場景

根據(jù)系統(tǒng)的功能處理過程，以及STPA方法論中所定義的分析引導(dǎo)圖。識別列車制動未實(shí)施的原因以及安全需求。

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

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

4 結(jié)論與未來工作

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

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