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

（卡斯柯信號(hào)有限公司北京分公司，北京 100160）

1 概述

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

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

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

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

2 STPA概述

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

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

圖1 STPA的步驟

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

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

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

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

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

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

3.3 步驟三：識(shí)別不安全的控制行為

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

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

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

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

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

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

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

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

表2 不安全的控制行為

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

圖4 致因場(chǎng)景

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

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

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

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

3.4 步驟四：識(shí)別致因場(chǎng)景

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

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

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

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

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

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