列控臨時限速場景風險耦合路徑自動搜索方法研究

高 僮，張亞東，郭 進，王 建

(西南交通大學信息科學與技術學院，成都 611756)

列車運行控制系統(tǒng)(以下簡稱列控系統(tǒng))是高速鐵路信號系統(tǒng)的關鍵技術和核心裝備，能有效保證列車安全、準時、舒適、高速、高密度不間斷運行，是高速鐵路的“大腦和中樞神經”[1]。列控系統(tǒng)作為安全苛求系統(tǒng)，一旦發(fā)生危險失效，將會導致非常嚴重的行車事故。因此，針對復雜交互作用下的列控系統(tǒng)運營場景，如何科學地分析危險事件間的風險耦合路徑，是列控系統(tǒng)安全領域亟待解決的問題之一。臨時限速場景是列控系統(tǒng)典型運營場景之一，如果未按計劃下達或下達錯誤的臨時限速信息，將可能導致重大行車事故，因此保證臨時限速場景的安全性，對于保障高速鐵路運營安全具有重要的意義[2]。

目前，針對列控系統(tǒng)的安全分析以及形式化建模驗證已有較多研究，周翔等[3]通過分析臨時限速命令擬定校驗、下達和執(zhí)行反饋等基本操作流程，結合信息之間的交互關系和交互方式，利用時間自動機理論建立了臨時限速場景的時間自動機網絡模型；胡雪蓮、周翔等[4-5]采用時間自動機理論和消息順序圖(MSC)相結合的方法，對列控系統(tǒng)不同運營場景進行了建模與驗證；周果等[6]以Markov決策過程為基礎集成列控系統(tǒng)的正常行為和失效行為提出了綜合系統(tǒng)行為模型CBM，并通過概率模型檢驗工具PRISM對危險失效概率進行了準確計算； DIRK S等[7]考慮到STAMP不包含形式化建模的缺陷，將深度危險分析方法ProFunD與Petri網模型相結合，并將其巧妙融入到STAMP中，且利用該方法對中國溫州7.23動車事故進行了實例分析。綜上，目前的研究主要集中在列控系統(tǒng)危險分析、形式化建模驗證或兩者結合的方面，而列控系統(tǒng)運營場景風險耦合路徑分析方法的研究相對少見。

以列控系統(tǒng)復雜運營場景之一(臨時限速)為研究對象，結合深度優(yōu)先搜索算法，對含有危險致因因素的臨時限速場景時間自動機模型進行系統(tǒng)位置遷移路徑自動搜索，得到列控系統(tǒng)臨時限速場景風險耦合路徑。采取的技術路線如圖1所示。

圖1 技術路線

為實現(xiàn)臨時限速場景風險耦合路徑的自動搜索，首先，按照STPA危險分析方法的實施流程，分步驟進行危險分析，得到臨時限速運營場景危險日志；同時，根據(jù)臨時限速場景描述和場景分層控制結構模型，利用時間自動機理論進行形式化建模，得到正常臨時限速場景時間自動機模型；然后，將STPA分析出的危險致因作為位置遷移條件注入到系統(tǒng)正常時間自動機模型中，得到了含有危險致因因素的列控系統(tǒng)臨時限速場景時間自動機模型；最后，利用自動搜索算法，編制了遷移路徑自動搜索工具軟件，利用軟件對含有危險致因因素的臨時限速場景時間自動機模型進行系統(tǒng)位置遷移路徑自動搜索，得到列控系統(tǒng)臨時限速場景風險耦合路徑。

1 相關基礎知識

1.1 列控系統(tǒng)臨時限速運營場景

臨時限速運營場景主要由調度員、CTC、TSRS、RBC以及TCC等子系統(tǒng)和人員相互交互，實現(xiàn)臨時限速命令的擬定、驗證、下達、執(zhí)行等過程。CTC系統(tǒng)主要負責擬定臨時限速命令，通過調度員在CTC終端輸入臨時限速命令參數(shù)信息，擬定臨時限速命令；TSRS統(tǒng)一管理系統(tǒng)的運行過程，其工作包括需對由CTC下達的臨時限速進行有效性檢驗[8]、對將要執(zhí)行的臨時限速命令向CTC發(fā)出激活提示、對臨時限速命令進行拆分與轉換等；最后，RBC和TCC執(zhí)行完臨時限速命令后，分別通過GSM-R網絡或有源應答器將臨時限速命令傳輸給列車[9]。

為更好的理解臨時限速運營場景的系統(tǒng)行為，通過圖2來展示臨時限速場景的一個設置階段過程。臨時限速場景的設置過程主要由3個階段組成，分別為臨時限速命令擬定、臨時限速命令驗證和臨時限速命令執(zhí)行。

圖2 設置臨時限速命令的操作時序

1.2 基于STPA的臨時限速運營場景危險分析

STPA方法辨識系統(tǒng)控制缺陷時遵循一系列的流程[10-13]，其流程如圖3所示。

圖3 STPA實施流程

基于STPA的臨時限速運營場景危險分析結合臨時限速運營場景的操作流程和STPA分析流程進行危險分析。

首先，確定系統(tǒng)級危險。對臨時限速的安全分析[14-15]中所要考慮的事故主要從兩個方面去考慮，一是對人造成了傷害[A1]；二是對設備造成了傷害[A2]。因此，臨時限速下的系統(tǒng)級危險如下。

H1：列車在需要收到臨時限速命令的情況下，未收到臨時限速命令。

H2：列車接收到了錯誤的臨時限速命令。

H3：列車在不需要收到臨時限速命令的情況下，收到了臨時限速命令。

相應的系統(tǒng)級安全約束如下。

SC1：列車在需要收到臨時限速命令的情況下，收到了臨時限速命令。

SC2：列車接收到正確的臨時限速信息。

SC3：列車在不需要收到臨時限速命令的情況下，未收到臨時限速命令。

根據(jù)圖2所示的臨時限速運營場景的操作流程構建分層控制結構模型。分層控制結構模型的最頂層由CTC和調度員組成，CTC通過向TSRS發(fā)送控制信息，約束TSRS的行為，而TSRS作為CTC的下一層，通過對臨時限速調度命令進行拆分和轉換，向在臨時限速調度命令所管轄范圍內的TCC和RBC發(fā)送臨時限速信息，因此，TCC和RBC作為TSRS的下一層。然后，TCC通過應答器、RBC通過GSM-R將臨時限速信息發(fā)送給列車，因此，應答器和GSM-R作為TCC和RBC的下一層，最后一層為列車。其中，各個子系統(tǒng)之間通過控制行為進行交互。

然后，通過對臨時限速運營場景的主要角色或要素的運行過程和控制行為進行分析，得到39個控制行為，根據(jù)STPA識別不安全控制行為的方法，即按照以下4種場景進行識別：未提供控制行為、提供了控制行為、錯誤時機或時序提供控制行為以及提供控制行為結束太快/時間過長。從而得到臨時限速運營場景的不安全控制行為列表。

最后，針對每一條不安全控制行為進行控制缺陷分析。先進行不安全控制行為的過程模型圖及致因因素分析，再結合專家提出的相關的安全約束，最終制定了臨時限速運營場景的危險日志。

1.3 含有危險致因因素的臨時限速場景時間自動機模型

構建臨時限速運營場景時間自動機模型方法的具體流程如圖4所示。

圖4 時間自動機模型構建方法

臨時限速運營場景時間自動機模型由CTC、調度員、TSRS、TCC、RBC等五部分組成，進程之間通過共享變量和通道來進行同步或通信。

根據(jù)設置臨時限速命令的操作流程描述以及通道和位置的命名，可以構建臨時限速場景正常的時間自動機模型。通過將1.2節(jié)分析得出的不安全控制行為的致因因素，作為位置遷移的條件注入到臨時限速場景正常的時間自動機模型中，從而得到了含有危險致因因素的臨時限速場景時間自動機模型。

根據(jù)1.2節(jié)得知，通過對設置臨時限速命令的操作流程進行描述，STPA進行初步評估，定義了39個控制行為，在STPA危險分析中將控制行為在分層控制結構模型中得以描述，可假定 39個控制行為與UPPAAL中的通道或位置進行一一對應，從而實現(xiàn)對STPA與時間自動機兩者之間建立聯(lián)系。關鍵的控制行為和對應的UPPAAL通道或位置如表1所示。

表1 關鍵控制行為和對應的UPPAAL通道或位置

本文主要側重于風險耦合路徑的搜索方法研究，由于篇幅原因，將以TSRS和TCC時間自動機模型為例進行方法研究和驗證。在兩個模型中，包含兩個危險事件，分別是：TSRS與TCC之間的信息安全數(shù)據(jù)網發(fā)送信息錯誤Send_IncorrectMess和TCC與LEU之間受到通信干擾communica_Jam。

1.3.1 含有危險致因的TSRS時間自動機模型

在時間自動機模型中，兩個圓代表了系統(tǒng)的初始狀態(tài)，一個圓代表系統(tǒng)的中間狀態(tài)，兩個狀態(tài)之間的帶有箭頭的線和上面的文字代表了兩個狀態(tài)轉換的約束條件，發(fā)出的信息用a!表示，接收的信息用a？來表示，a表示為該消息擬定的名稱，若名稱相同，則表示為同一組消息[16]。

構建含有危險致因的TSRS時間自動機模型時，當完成臨時限速命令的有效性校驗以及激活驗證后，向調度員下達執(zhí)行提示，TSRS再次拆分和轉換臨時限速命令，發(fā)送至對應的TCC和RBC進行臨時限速命令的執(zhí)行性檢驗[17]。其中，TSRS與TCC之間的信息安全數(shù)據(jù)網出現(xiàn)發(fā)送信息錯誤Send_IncorrectMess，狀態(tài)轉移到安全數(shù)據(jù)網故障狀態(tài)Safety_DataNetError；發(fā)送信息正常時Send_CorrectMess，狀態(tài)轉移到安全數(shù)據(jù)網正常狀態(tài)Safety_DataNetNor。不論是正常狀態(tài)還是故障狀態(tài)，都要將臨時限速命令發(fā)送給TCC進行執(zhí)行性檢驗。含有危險致因的TSRS時間自動機模型如圖5所示。

圖5 含有危險致因的TSRS時間自動機模型

1.3.2 含有危險致因的TCC時間自動機模型

在構建含有危險致因的TCC時間自動機模型中，對臨時限速命令進行有效性檢驗，檢驗成功后，將對臨時限速命令開始執(zhí)行性檢驗。其中，TSRS與TCC之間的信息安全數(shù)據(jù)網出現(xiàn)發(fā)送信息錯誤Send_IncorrectMess，狀態(tài)轉移到安全數(shù)據(jù)網故障狀態(tài)Safety_DataNetError；發(fā)送信息正常時Send_CorrectMess，狀態(tài)轉移到安全數(shù)據(jù)網正常狀態(tài)Safety_DataNetNor。無論是正常或故障狀態(tài)都要將命令發(fā)送給TCC進行執(zhí)行檢驗，若TCC未檢驗出數(shù)據(jù)錯誤仍實現(xiàn)檢驗成功，則向TSRS返回TCC_exeSucc消息，此時當TCC與LEU之間通信網絡受到干擾communica_Jam，那么狀態(tài)轉移到Communica_Error，接著TCC將發(fā)送錯誤的臨時限速命令給車載設備。含有危險致因的TCC時間自動機模型如圖6所示。

圖6 含有危險致因的TCC時間自動機模型

2 遷移路徑自動搜索算法

DFS用于搜索指定的頂點或是對圖進行遍歷，是一個遞歸并伴有回退的過程[18-20]。

將時間自動機模型的位置等價為有向圖的頂點，將時間自動機模型的遷移路徑等價為有向圖的弧，可將時間自動機模型等價為帶有自環(huán)弧的多重弧有向圖。基于此，利用DFS，結合時間自動機模型，提出基于DFS的遷移路徑自動搜索算法。

基于DFS的遷移路徑自動搜索是一個遞歸過程，基本思想為：從時間自動機的起始位置開始，訪問尚未訪問過的一條出發(fā)遷移，到達另一位置作為當前位置，再訪問當前位置尚未訪問過的一條出發(fā)遷移，重復上述過程，直到當前位置不存在尚未訪問過的出發(fā)遷移，則將當前訪問過的遷移作為一條遷移路徑；如果該路徑的某個遷移包含危險致因因素，則將其作為一條結果遷移路徑；然后，從當前位置去除一個遷移回退到上一個位置，將其作為當前位置，繼續(xù)訪問尚未訪問過的出發(fā)遷移，直到所有的遷移全部被訪問過，即得到結果遷移路徑集合。基于DFS的遷移路徑自動搜索算法流程如圖7所示。

圖7 基于DFS的遷移路徑自動搜索算法流程

基于DFS的遷移路徑自動搜索的具體算法如下。

輸入：時間自動機模型

輸出：遷移路徑集合

(1)定義已覆蓋遷移的集合coverSet，遷移路徑path和結果遷移路徑集合pathSet；

(2)令初始位置為location；

(3)DFS (location) ；

(4)if(存在未包含在coverSet中的location的出發(fā)遷移)；

(5)對于未被覆蓋的location的每條出發(fā)遷移transition；

(6)將transition加入到path末尾及coverSet中，并令path的末尾位置為location；

(7)DFS (location)；

(8)從path的尾部移除一個遷移；

(9)else若path中的某個遷移包含危險致因因素，將當前path添加到pathSet中；

(10) return pathSet。

3 系統(tǒng)位置遷移路徑自動搜索工具軟件

Qt是一個跨平臺C++圖形用戶界面應用程序開發(fā)框架，基于DFS的遷移路徑自動搜索算法，利用Qt實現(xiàn)遷移路徑生成工具軟件的開發(fā)。工具軟件界面如圖8所示，包含兩個區(qū)域，左邊為用戶選擇區(qū)，供用戶選擇文件、模型及運算算法等；右邊為結果輸出區(qū)，用于展示搜索出的遷移路徑。

圖8 位置遷移路徑生成工具

位置遷移路徑生成工具的原理流程為選擇xml文件，讀取模型，用DFS運算路徑，按4個步驟輸出結果，如圖9所示。

圖9 工具的原理流程

4 危險位置遷移路徑生成

選擇含有危險致因的臨時限速模型的xml文件，讀取TSRS時間自動機模型，得到DFS運算的路徑共5條，如圖10所示。

圖10 含有危險致因的TSRS的DFS算法路徑

選擇含有危險致因的臨時限速模型的xml文件，讀取TCC時間自動機模型，得到DFS運算的路徑共5條，如圖11所示。

圖11 含有危險致因的TCC的DFS算法路徑

5 風險耦合路徑的生成

通過第4章使用DFS算法，針對含有危險致因的臨時限速場景時間自動機模型進行位置遷移路徑自動搜索的結果得到的風險耦合路徑有兩條，如下所示。

路徑3：

Idle->order_to TCC？; T7:=0;->TCC_Test

TCC_Test->T7<=T_TCCreaction;TCC_testResult!;->TCC_TResult

TCC_TResult->TCC_returnSucc!;->verify_Succ

verify_Succ->Send_CorrectMess？;->Safety_ dataNetNor

Safety_dataNetNor->distribute_ToTCC？;T8:=0;->TCC_Execute

TCC_Execute->T8>T_TCCreaction;->verify_ Succ

verify_Succ->Send_IncorrectMess？;->Safety_ dataNetError

Safety_dataNetError->distribute_AbnToTCC？; T8:=0;->TCC_Execute

TCC_Execute->T8<=T_TCCreaction;TCC_exeResult!;->TCC_EResult

TCC_EResult->TCC_exeSucc!;->Execute_succ

Execute_succ->communica_Jam？;->Communica_Error

Communica_Error->error_To Tras!;->order_to Tras

order_to Tras->To Train？;->Tras_to Train

Tras_to Train->->Idle

在這條路徑中，TCC在激活驗證成功后，TSRS與TCC之間的信息安全數(shù)據(jù)網出現(xiàn)發(fā)送信息錯誤Send_IncorrectMess，狀態(tài)轉移到安全數(shù)據(jù)網故障狀態(tài)Safety_dataNetError，TCC收到異常的臨時限速執(zhí)行命令distribute_AbnToTCC；TCC進行執(zhí)行性校驗狀態(tài)，TCC校驗完成后，由于TCC自身邏輯發(fā)生故障，向TSRS返回校驗成功標志TCC_exeSucc；與此同時，TCC與LEU之間受到通信干擾communica_Jam，TCC將錯誤的臨時限速命令通過LEU發(fā)送給有源應答器，且TSRS認為目前正在執(zhí)行正確的臨時限速命令，對列控系統(tǒng)有非常大的安全隱患。此危險是由TCC和TSRS之間安全數(shù)據(jù)網發(fā)送信息錯誤，TCC自身邏輯發(fā)生故障，TCC與LEU之間受到通信干擾等3個危險致因相互耦合作用下發(fā)生。

路徑4：

Idle->order_to TCC？; T7:=0;->TCC_Test

TCC_Test->T7<=T_TCCreaction;TCC_testResult!;->TCC_TResult

TCC_TResult->TCC_returnSucc!;->verify_Succ

verify_Succ->Send_CorrectMess？;->Safety_ dataNetNor

Safety_dataNetNor->distribute_ToTCC？;T8:=0;->TCC_Execute

TCC_Execute->T8>T_TCCreaction;->verify_ Succ

verify_Succ->Send_IncorrectMess？;->Safety_ dataNetError

Safety_dataNetError->distribute_AbnToTCC？; T8:=0;->TCC_Execute

TCC_Execute->T8<=T_TCCreaction;TCC_exeResult!;->TCC_EResult

TCC_EResult->TCC_exeSucc!;->Execute_succ

Execute_succ->communica_notJam？;->Communica_Norm

Communica_Norm->To Tras!;->order_to Tras

在這條路徑中，TCC在激活驗證成功后，TSRS與TCC之間的信息安全數(shù)據(jù)網出現(xiàn)發(fā)送信息錯誤Send_IncorrectMess，狀態(tài)轉移到安全數(shù)據(jù)網故障狀態(tài)Safety_dataNetError，TCC收到異常的臨時限速執(zhí)行命令distribute_AbnToTCC；TCC進行執(zhí)行性校驗狀態(tài)，TCC校驗完成后，由于TCC自身邏輯發(fā)生故障，向TSRS返回校驗成功標志TCC_exeSucc；雖然此時TCC與LEU之間通信未受到干擾communica_notJam，TCC依舊將異常的臨時限速命令distribute_AbnToTCC通過LEU發(fā)送給有源應答器，且TSRS認為目前正在執(zhí)行正確的臨時限速命令，對列控系統(tǒng)有非常大的安全隱患。此危險是由TCC和TSRS之間安全數(shù)據(jù)網發(fā)送信息錯誤，TCC自身邏輯發(fā)生故障兩個危險致因相互耦合作用下發(fā)生。

6 結論

綜合運用STPA危險分析方法和時間自動機理論，結合深度優(yōu)先搜索算法，提出了列控運營場景風險耦合路徑自動搜索方法。以列控系統(tǒng)臨時限速場景為研究對象，對含有危險致因因素的臨時限速場景時間自動機模型進行系統(tǒng)位置遷移路徑自動搜索，最終得到列控系統(tǒng)臨時限速場景風險耦合路徑。該研究有助于深入揭示列控系統(tǒng)復雜的危險致因機理，為風險預警及安全管控提供科學支撐，對于提高列控系統(tǒng)的運營安全性、保障高速鐵路行車安全具有重要的理論意義和應用價值。