基于STPA和時序邏輯的RBC切換場景安全分析

林經源 何濤

（1.蘭州交通大學自動化與電氣工程學院 甘肅省蘭州市 730070）

（2.蘭州交通大學自動控制研究所 甘肅省蘭州市 730070）

隨著中國高鐵技術的不斷完善和升級，高鐵在人民的出行中占據了越來越重要的地位，這也意味著一旦高鐵行車過程中出現危險，會對人民的生命財產安全造成嚴重威脅。為滿足我國鐵路運輸日益增長的運營需求，在保證安全的前提下，我國在列車控制系統領域博采眾長，自主開發了 CTCS（Chinese Train Control System，中國列車控制系統）。其中我國現行高速鐵路主要干線中使用的是CTCS-3 級列控系統（下簡稱為C3 系統）。為保證安全性、可靠性、可用性和穩定性等各方面性能，我國對C3 系統有著嚴格的要求，以國際標準IEC61508為標準，CTCS-3 級列控系統設計使用前需要經過嚴格的安全分析與測試工作，為了保證系統在均滿足現行規范要求，進而保障人們生命和財產安全。

現有大部分針對復雜系統的安全性分析中，故障樹分析，故障模式及影響分等方法將系統的安全性問題拆分，由多個組件的可靠性來保證最終復雜系統的安全性。這些方法了較好的效果，但是這些方法難以針對復雜系統中的多個組件交互中可能出現的安全問題進行分析。系統理論過程分析將安全性問題轉化為控制問題，能夠針對多個組件間的相互作用中可能出現的安全性問題進行分析，在航空，醫療，交通，項目管理等領域的安全性分析中進行了廣泛的應用，取得了一定的成就。

根據現場實際運行情況來看，列控系統組件和功能復合度較強，現行分析中針對各個組件的分析已經不能較好的描述現場中出現的多組件之間的共同作用的復合故障，本文基于STPA 分析，并且使用時序約簡，提出一種尋找復合故障可能出現情況的方法，為實際現場測試提供參考。

1 基本理論

1.1 STPA原理

系統理論的過程分析(System-Theoretic Process Analysis,STPA)由Leveson 于2003年提出[1]。 這種方法基于系統理論事故建模和過程(Systems-Theoretic Accident Modeling and Processes，STAMP)，是一種近幾年來發展迅速的新型安全分析方法。

STAMP 采用分層控制結構來描述部件間的控制關系，如果這些控制能滿足安全約束條件則系統是安全的。在STAMP 理論中指定一下4 種不恰當控制關系：

（1）控制器沒有提供本應提供的控制行為，或控制行為沒有被很好地執行，可以用N(Not Provided)來記錄；

（2）控制器錯誤提供了控制行為或提供了不安全的控制行為，記錄為I(Incorrect)；

（3）控制行為出現在錯誤的時間，即過早(E,Early)或者過晚(L,Late)；

（4）正確的控制行為停止的過早或持續過久，即持續時間(T,time)問題。

STPA 旨在發現以上不恰當控制關系，并對其成因加以分析。其分析步驟如圖1所示。

圖1：STPA 的實施步驟

STPA 可有效從控制的角度對系統的不恰當行為進行分析，但是列控系統作為多控制器的復雜控制系統，部件間有復雜的時序邏輯關系。考慮一個控制行為是否恰當還需針對其觸發的時序邏輯進行分析，而STPA 方法難以進行詳細的時序邏輯描述。我們需要一種針對控制行為的時序邏輯情況進行分析的完成不恰當行為的辨識。

1.2 基于時序邏輯的不恰當行為分析方法

一般而言，控制命令本身是有時間的，STAMP 中第四條控制風險就是針對存在控制命令本身有較長持續時間的情況，但是在列控系統中，大部分控制命令下達是為一個具體時點。控制行為發生后就已經引起了系統的變化，本文再討論時序邏輯描述時將控制行為發生的時點進行定位，討論一個控制行為在對應時點上是否已經發生，故暫時不考慮控制行為持續時間的問題。

本文使用邏輯是與非（?）來表現控制命令情況是否與描述一致。因實際運行中時序邏輯關系較為復雜，故在此引入布爾邏輯符號且（∧）和或（?）來描述兩控制命令同時發生和兩事件均獨立發生。具體的參考時間點放在最后，用“|”隔開，表示該時間點前是否發生。則“列車依次實施常用制動（SB）和緊急制動（EB）”可以被描述為SB|EB，即是在緊急制動發生時，常用制動已經發生。

因德摩根律在經典命題邏輯的外延中依然有效，我們可以根據德摩根律歸納一系列的約簡法則來約簡實際情況中較為復雜的時序邏輯關系。其約簡法則如下所示：

這里針對式1-1 給出證明：設x 為t 時間點前的時刻，則：

式1-1 證畢。

因實際時間節點選取更復雜和靈活，在這里補充兩個時序表達式約簡方法，以針對復雜時許情況下同一事件多次出現的情況：

這里對式1-3 給出證明：設A 事件發生的時間為T，則：

式1-3 證畢。

當多個事件發生在同一個時點的時候，事件關系與這個統一時點無關，則顯然有以下時序邏輯關系：

通過這些時序邏輯約簡方法，我們可以將實際問題中復雜的時序邏輯關系進行化簡，從而為后續不恰當控制行為的簡化和求解提供理論支持。

2 列控系統的STPA分析

2.1 確定系統級危險和安全約束

CTCS-3級列控系統作為實際控制列車運行的系統，其主要功能是保證列車在運行過程中不會出現危險事故。鐵路事故一般由內部事故和外部事故兩部分組成。內部事故包括系統內部的具體的組件故障，產生的錯誤命令等情況出現的事故。需要由列控系統保證自己的可靠性和安全性。外部事故一般是由外部環境的變化導致的，例如障礙物等，需要列控系統即使分析識別并且做出應對，因其發生情況復雜多變，只能根據實際事故情況進行分析。對于內部事故而言，一般為列車追尾事故或列車脫軌事故，其本質是列控系統未能保證列車不超過安全速度，或者列控系統未能保證安全距離[2]。以此為基礎，系統安全約束為“列控系統需保證列車行駛不超過安全速度和安全距離”。

2.2 系統分層控制模型的建立

在STAMP 的系統理論事故模型中，系統通過分層控制來保證系統能保持動態平衡，并且可以根據外部環境做出應對[3]。當系統及其組件均被正常控制時，系統被視為是安全的。我們需要根據實際的列控系統控制結構和控制行為建立對應的模型，分析系統的不恰當的控制行為。CTCS-3 級列控系統構成及接口圖如圖2所示。

圖2：CTCS-3 級列控系統構成及接口圖

針對圖2 的實際CTCS-3 級列控系統構成及其接口[4]，其分層控制關系模型構建如下：

如圖3所示，C3 列控系統控車過程復雜，多組件協同工作情況多，相關的控制關系也較為復雜，我們需要根據分析的場景分解整體結構，選擇具體的場景涉及到的相關組件和控制關系進行分析。CTCS-3 級列控系統有十四個主要運營場景，現行測試中針對單獨場景的測試已經較為完備，但實際運行中情況更復雜，多運營場景間互有交叉，需要具體場景具體進行分析。下面就針對具體過程進行細化分析。

圖3：CTCS-3 級列控系統分層控制系統模型圖

2.3 RBC切換場景STPA分析

本文以列控系統中較為復雜的RBC切換場景為例，對其進行具體的安全性分析。在確定系統級危險后，我們需要結合列控系統分層控制系統模型與具體的運營場景[5]，建立對應的系統分層控制結構框圖。

接下來，我們需要將系統級危險行為細化，在RBC切換過程中找到可能導致最后超出安全速度或者侵入安全距離的具體危險行為。為此需要將RBC 切換運營場景中的所有行為及時序順序進行描述。

根據在此運營場景中的時序順序描述，我們可以將系統級危險對每一個時序過程中可能出現的問題進行分解，這里以在制動命令的產生的時刻為例：

Speed:iVLocagtion:i=reqSB:n|speed>sbi∧reqEB:n|spe ed>ebi ? reqSB:l|speed>sbi∧reqEB:l|speed>ebi……

因行車速度超速的情況下，常用制動速度低于緊急制動速度，其時點也對應更早。所以在此式中speed>sbi的時點一定在speed>ebi 之前，故可以將原式簡化如下

Speed:iVLocagtion:i=reqSB:n|speed>sbi∧reqEB:n|spe ed>sbi ? reqSB:l|speed>sbi∧reqEB:l|speed>sbi……

這里就可以應用先前的約簡公式，將該式約簡為：

Speed:iVLocagtion:i=(reqSB:n ? reqEB:n)|speed>sbi ?(reqSB:iVreqEB:i)|speed>sbi……

在此例中，與reqSB，reqEB 相關的部分均以化簡結束，即在這個環節中，常規制動命令和緊急制動命令有關的危險情況均已分析完成，即超過限制速度時，緊急停車。

命令均未提供或兩命令均過晚，在此化簡基礎上，因常用制動一定在緊急制動發生之前，在這里可以在最后對常用制動與緊急制動之間這段約束進行約簡，可以將其化簡為：

Speed:iVLocagtion:i=reqSB:n| reqEB:n ?reqSB:l|reqEB:l……

按以上過程，我們對時序圖中所有有可能造成系統安全風險的過程進行展開和簡化，RBC 切換過程中所有的不恰當控制行為化簡結果如表1所示。

表1：RBC 切換場景時序約簡結果及含義

經上述化簡后，我們得到了RBC 切換這個實際運營場景下有可能造成危險結果的不恰當控制行為。這些行為有具體的時點和錯誤的控制情況，設計人員在設計相關功能時，需要考慮這些時點的不安全行為，從而更好地保證系統安全。同時，在后期測試工作中，也應針對可能導致這些時點出現不恰當控制行為的情況予以考慮，從而更加周密的完成測試，提高測試效率。

3 結束語

傳統安全分析方法受制于由故障組件開始的安全分析，多關注與具體的某個組件故障后對系統安全性的影響，本文給出了自上而下的控制行為辨識方式，輔以時序邏輯分析，在保證危險控制行為辨識準確性的同時，盡可能的考慮了控制行為間時序對不恰當控制行為的影響，并以RBC 系統切換為例進行了分析，得出了RBC切換運營場景下的具體不恰當控制，為安全系統設計者和安全系統測試者提供參考。