基于STAMP與模型檢驗的全自動無人駕駛復雜運營場景安全驗證方法

馬牧云，張亞東，2，李 耀，郭 進，2

(1.西南交通大學信息科學與技術學院,成都 611756; 2.四川省列車運行控制技術工程研究中心,成都 611756;3.成都信息工程大學軟件工程學院,成都 610225)

引言

近年來,隨著城市人口數量不斷攀升,交通運輸的壓力也隨之增大,軌道交通能夠有效改善城市發展中的交通擁堵、污染等問題,得到了飛速發展。全自動無人駕駛系統作為智慧城市軌道交通的核心技術裝備之一,由于其較高的自動化程度和智能化水平而得到了廣泛發展與應用[1-2]。與傳統軌道交通控制系統相比,全自動無人駕駛系統能夠提高行車效率,減少或取消人工操作,系統運營場景涵蓋了列車自動喚醒、自動正線運營、進站停車、自動折返以及故障情況下自動恢復等數十個正常運營場景和異常場景[3]。不同運營場景下,全自動無人駕駛系統具有不同的交互主體、交互行為和控制邏輯,系統危險及致因具有較強的隱蔽性和復雜性,給運營安全帶來了新的挑戰。如何驗證全自動無人駕駛復雜運營場景下的系統安全性,已經成為全自動無人駕駛技術迫切需要解決的關鍵問題之一。

傳統的安全分析方法主要是基于線性事件鏈的系統安全理論和方法[4-5]。但隨著計算機、通信等技術與安全苛求系統的不斷融合,系統的復雜度和耦合度急劇上升,系統危險形式與危險致因場景呈現出更加多樣化、隱蔽性與復雜化等特點,安全驗證的難度驟然增大。系統事故的發生不再由單一的或幾個危險事件線性疊加的結果來決定,因此,基于線性事件鏈的傳統安全分析方法表現出了一定的局限性。為應對此類問題,2004年,Nancy Leveson提出了STAMP理論[6]。將系統視為一種分層控制結構,將安全問題轉換為控制問題。之后基于STAMP理論,Leveson進一步提出STPA(System Theoretic Process Analysis)方法用于危險致因分析,這種方法采用自上而下的分析手段,能夠更加系統地進行危險分析,更全面地辨識出所有會使系統進入危險狀態的致因因素[7-8]。STAMP理論在系統安全領域得到了廣泛發展和應用。文獻[9]以列車進站停車以及站臺發車異常運營場景為例,研究應用STAMP理論與STPA方法,對潛在的不安全控制行為及危險致因進行了辨識。然而,由于STAMP模型采用自然語言,缺乏形式化手段,存在模糊或歧義的問題且模型無法自動驗證。針對以上問題,文獻[10]結合時間自動機,探索了STPA-UPPAAL的轉換規則以及分析規范,通過時間自動機模型,驗證了系統的不安全控制行為,提高了不安全控制行為的驗證效率。文獻[11]結合有色Petri網,利用CPN模型對系統進行形式化建模,避免了自然語言的二義性,以高鐵列控為例,進行了形式化驗證。與以上建模方法相比,安全狀態機作為圖形化的同步建模語言,模型清晰、簡潔,具有良好的可讀性,能夠用嚴格的語義避免需求描述的模糊性和二義性等缺陷。同時,高安全性應用開發環境SCADE[12],支持安全狀態機的建模、仿真及驗證。目前SCADE工具和安全狀態機已在車站計算機聯鎖系統、列控系統等安全苛求系統的軟件建模與驗證方面具有了良好的應用基礎。

本文基于STAMP系統安全分析理論,引入安全狀態機建模方法,提出了一種基于STAMP理論與模型檢驗相結合的復雜運營場景安全驗證方法。

1 安全分析及驗證理論基礎

1.1 STAMP理論與STPA方法

STAMP理論是基于系統理論和控制理論的事故致因模型。其中重要的3個要素是:安全約束、分層安全控制結構和過程模型,安全約束作為3個要素中最基本的概念,需要被正確有效地執行[13]。在構建分層控制結構模型的過程中,充分考慮組織管理,系統交互等對系統安全的影響。根據系統理論,高層次結構部分的操作復雜性由低層次結構的操作決定。高層次的約束就是對低層次的控制。在STAMP理論的基礎上,Leveson提出的STPA主動分析方法用于危險致因分析,通過分析開發過程中潛在的危險致因因素,達到消除或控制危險源的目的。這種方法將分析過程主要分為以下幾個步驟:分析系統級危險、構建分層控制結構模型、辨識不安全控制行為、分析危險致因因素、制定相應的安全約束[14]。在STPA方法中,實施不安全的控制行為會導致系統進入危險狀態。在識別不安全控制行為時,常用的有以下4種分類[15]:

(1)未提供控制行為導致危險;

(2)提供錯誤的控制行為導致危險;

(3)提供控制行為的時間過早或過晚導致危險;

(4)控制行為作用的時間過長或過短導致危險。

1.2 安全狀態機建模與模型檢驗方法

安全狀態機(SSM)是一種圖形化的建模語言,具有并發性、層次性和通信機制[16]。主要由狀態和遷移兩部分組成,有激活和未激活兩種狀態。遷移有兩種屬性,分別為條件和行為(也就是賦值語句),位于遷移線上的行為只在遷移觸發時執行。位于狀態機內部的行為,需要在該狀態激活的每一個周期執行。狀態機要從當前狀態遷移至下一個狀態,需要同時滿足3個條件,一是當前狀態處于激活態,二是滿足遷移條件,三是需要滿足遷移的優先級。一個操作符可以包含一個或多個狀態機,狀態機之間可以是并行或者嵌套的關系。如圖1所示,該模型有兩個狀態,其中加粗邊框為初始狀態,如果在滿足遷移條件ON=true的情況下,狀態遷移觸發,從START狀態遷移至END狀態。遷移發生的順序根據遷移線設置的強遷移、弱遷移、同步遷移以及層次結構和優先級而有所不同。安全狀態機模型可以在仿真界面通過修改遷移條件的值進行單步仿真,初步解決模型的設計問題。

圖1 基礎安全狀態機模型

安全狀態機的驗證環境SCADE,目前多用于開發嵌入式安全關鍵系統的軟件。經過30多年的發展,逐漸在航空航天、國防軍工、汽車電子等行業具有了廣泛應用[17-19]。SCADE能夠覆蓋軟件開發的全部流程[20]。SCADE建模分為安全狀態機模型和數據流圖模型,都屬于圖形建模方法。兩種方式不是獨立存在的,可以結合使用。二者相比較,狀態機更適用于控制流方面的建模,在同樣精準地描述控制算法的前提下,更加易于擴展維護[21]。

2 場景安全驗證方法流程

2.1 場景安全驗證方法流程

基于STAMP理論與模型檢驗的復雜運營場景安全驗證框架主要包括三部分:基于STAMP理論和STPA方法的運營場景安全分析、運營場景安全狀態機形式化模型的構建、運營場景的形式化安全驗證?？傮w驗證框架如圖2所示。

圖2 總體驗證框架

本文的驗證過程主要分為以下5個步驟。

步驟1:運營場景分層控制結構模型的構建。針對具體運營場景,首先確定可能發生的系統級事故及危險,提取運營場景中涉及到的控制器、執行器、傳感器、被控過程以及交互信息等建模要素,遵循分層控制結構模型自上而下的建模順序,確定頂層控制器,并根據各個組件的信息交互行為,逐級構建運營場景的分層控制結構模型。以便后續分析導致系統層面危險發生的致因因素。

步驟2:辨識導致危險發生的不安全控制行為。分層控制結構模型表現了系統或場景中控制器和執行器的控制行為,結合分層控制結構模型以及相關場景規范,通過上述4種不恰當控制行為的分類,辨識場景中的不安全控制行為。

步驟3:危險致因分析及安全約束提取。針對潛在的危險,結合分層控制結構模型,構建過程模型細化分析,確定導致不安全控制行為發生的致因因素,并提取相應的安全約束。

步驟4:運營場景安全狀態機建模。通過提取運營場景分層控制結構模型中的模型要素,基于分層控制結構模型與安全狀態機模型之間的轉換規則,充分考慮運營場景安全約束,利用安全狀態機建模方法,在SCADE環境中,構建可形式化驗證的安全狀態機模型。

步驟5:運營場景安全驗證。利用數據流圖建模方法,針對提取的運營場景安全約束,構建相應的安全屬性模型,通過SCADE形式化工具,結合模型檢驗技術,對運營場景下的安全狀態機模型進行形式化安全驗證。

2.2 分層控制結構模型與安全狀態機模型間轉換規則

根據分層控制結構模型與安全狀態機模型的定義和特點,給出了兩種模型之間的基本轉換規則定義。在構建的過程中,變量的名稱可以根據實際所需要的內容自行定義,結合實際設計方式進行擴展。

當安全狀態機的一個狀態創建完成后,需要對其屬性進行設置,通常包括狀態機名稱、起始狀態以及終止狀態等。轉換過程的第一步需要根據狀態機的狀態內行為設計方式的不同,將狀態機劃分為4種類型[22],分別如下。

(1)無行為邏輯的狀態機,也就是沒有添加行為邏輯的狀態機。

(2)嵌套基于模型設計的狀態機,用于行為元素能夠被狀態布局完全容納的情況下,常見于將數據流圖嵌套于狀態機內。

(3)嵌套SCADE文本設計的狀態機,用于控制行為便于用SCADE文本表達的情況。

(4)隱藏文本內容的狀態機,用于行為元素無法被狀態布局容納的情況下。

分層控制結構模型能夠表現待分析系統或場景中交互主體的通信關系、信息交互內容等。其核心結構有控制器、執行器、傳感器、被控過程等?；诖?定義以下規則,模型轉換基本原則如圖3所示。

圖3 模型轉換規則示意

規則1:控制器需要接收高層次部件發出的命令,并向低層次部件發出命令,針對控制器的行為邏輯,將其構建為嵌套SCADE文本的SSM。

規則2:系統中執行器需要發送信息至下一級控制器或自身狀態需要根據接收到的命令改變,針對執行器的行為邏輯結合實際場景,將其構建為嵌套SCADE文本的SSM或嵌套基于模型設計的SSM。

規則3:傳感器作為兩層控制器之間的信息反饋裝置,根據需要反饋的信息類型,結合實際場景構建為無行為邏輯的SSM或嵌套基于模型設計的SSM。

規則4:被控過程構建為無行為邏輯的SSM。

規則5:控制器發出或接收的命令、執行器需要執行的命令以及自身狀態變化、組件間的交互信息、傳感器反饋的信息等內容被提取為遷移條件或遷移行為,當信息內容為時序相關或只需要在遷移觸發時執行的,將其構建為BOOL表達式,位于遷移線上;當信息內容需要在狀態激活時的每一個周期執行時,例如一個控制器處于激活態時,它就需要發送相應的命令至下一級控制器或執行器,諸如此類的命令信息可以將其設置為枚舉或其他類型,構建為SCADE賦值語句嵌套于對應的SSM中。

3 列車自動進站停車場景安全分析

進站停車場景是全自動無人駕駛場景中正線運營時的場景之一。當列車確認收到滿足進站條件的移動授權,站臺門關閉,緊急停車按鈕未按下,人員防護開關SPKS置于非防護位,這4個條件滿足時,列車可以進站。在該場景中列車需要完成自動駕駛進站精準停車;欠標或過標時根據距離的不同,設置不同的運行模式最終對標停車;安全打開站臺門及車門,確保車門與站臺門對位隔離,對應打開或關閉。

3.1 列車自動進站停車場景描述

根據相關技術規范,對列車進站停車場景進行描述[23-24]。該流程包括參加系統活動的對象,主要是各個子系統及設備。主要的交互信息如圖4所示。

圖4 進站停車場景活動圖

場景主要流程說明如下。

(1)控制中心將線路相關信息發送至車載控制器VOBC,并提供臨時限速。

(2)車載控制器VOBC確認線路信息并發送列車相關信息至區域控制器ZC,ZC需確認收到并根據信息計算移動授權MA。

(3)當確認收到移動授權,站臺門關閉,緊急停車按鈕未按下,人員防護開關SPKS置于非防護位,這4個條件滿足后,列車可以進站停車。

(4)輸出制動,判斷車輛停車位置是否位于允許范圍內,若未超過允許范圍,停車成功;若車輛超過允許范圍,先輸出緊急制動,判斷車輛過標/欠標是否超過5 m,若未超過5 m,則緩解緊急制動,并自動調整對標停車;若超過5 m,則不能緩解緊急制動,并通知人工上車救援,以人工模式停車。

(5)判斷車輛速度為0后,判斷站臺門是否發生故障,若發現故障,則及時屏蔽相應的車門。車載控制器VOBC向車門控制器發送開門信息,向計算機聯鎖系統CI發送站臺門打開信息。

(6)車門控制器收到信息并打開車門,確認狀態,向車載控制器VOBC反饋信息;同時計算機聯鎖系統發送開門信息至站臺門控制器,站臺門控制器收到信息打開站臺門并確認狀態,反饋至計算機聯鎖系統。

(7)控制中心向站臺廣播系統發送信息,站臺廣播進行播報。

3.2 列車進站停車危險分析

根據進站停車場景分析,可能發生的系統級事故如下。

A1:乘客受傷(開關門過程中夾傷等)。

A2:列車追尾。

A3:列車與障礙物相撞。

事故A1的相關危險主要是在列車車門開關過程中出現的,可能由于列車車門動作的異常,例如,車門的開啟時間異?；驔]有及時屏蔽出現故障的車門。針對事故A2和A3,列車運行時,通過接收區域控制器發送的移動授權,確定列車停車的目標點。當列車運行速度超過了能夠防護本列車在前方列車車尾或障礙物前停車的速度最大值時,將會導致危險。

針對上述三類事故,給出在進站停車場景中的系統級危險如下。

H1:車門動作異常(可能導致A1)。

H2:列車進站時超速(可能導致A2、A3)。

3.3 系統分層控制結構模型

根據對列車自動進站停車場景流程的定義和分解,提取場景中擔任控制器、執行器、被控過程的部分,在進站停車場景中,主要的上層控制器為車載控制器、控制中心、區域控制器、計算機聯鎖。各控制器需要發送相關指令或場景所需要的信息至下一層結構。車門控制器及站臺門控制器擔任執行器的作用,處理上層控制器發送的命令并對下一層的控制器或執行器發出指令。車門、站臺門及列車根據實際場景需求,提取為被控過程進行建模。構建完成的分層控制結構模型如圖5所示。

圖5 進站停車分層控制結構模型

3.4 不安全控制行為

根據分層控制結構模型中各控制器的控制行為,并結合以下4種通用分類,辨識不安全控制行為UCA(Unsafe Control Action),由于本文篇幅限制,表1給出了部分辨識結果。

表1 部分不安全控制行為辨識結果

3.5 致因分析

以H1為例,給出部分致因分析結果及安全約束如表2所示。首先構建針對車門控制的過程模型,如圖6所示。

表2 部分致因分析結果及安全約束

圖6 車門控制過程模型

4 列車自動進站停車場景的安全狀態機建模與安全屬性驗證

4.1 進站停車場景的安全狀態機模型

根據進站停車場景流程以及提煉的主要建模步驟,首先確定安全狀態機模型的基本框架,同時充分考慮安全分析中提取的安全約束內容,通過對進站停車場景的分層控制結構模型的定義和分解,分別提取在進站停車場景的分層控制結構模型中擔任控制器、執行器、傳感器以及被控過程的部分,利用上述定義的兩種模型之間的轉換規則,設置安全狀態機的形態;提取的通信信息的部分,根據時序類、命令類或被控部分自身狀態變化等實際情況的需要,構建為遷移條件或位于狀態內的賦值語句。安全狀態機模型部分變量類型及含義如表3所示,構建完成的安全狀態機模型如圖7所示。

表3 部分變量類型及含義

圖7 進站停車場景的安全狀態機模型

4.2 安全屬性模型構建

以系統級危險H1為例,給出安全驗證的過程。由上述安全分析可知,STPA識別的針對H1的不安全控制行為如下。

UCA1:緊急制動未緩解時車門開啟。

UCA2:站臺門發生故障時未隔離相應車門。

由于緊急制動未緩解,在該場景中是因為列車欠/過標5 m以上導致的,此時并未申請人工救援,列車不處于安全停車范圍內,如果此時打開車門將會導致危險。

針對UCA1,提取安全約束:“列車緊急制動未緩解時,VOBC不能發送開門信息至車門和CI”,進行形式化驗證分析。針對UCA2,提取安全約束:“檢測到站臺門故障未隔離相應車門時,VOBC不能發送開門信息至車門和CI”,進行形式化驗證分析。

以UCA1的安全約束為例,涉及到模型中的變量有:車載控制器發送開門信息(VOBC_Door_Message)和列車緊急制動(Em_Breaking)。當模型輸出為true,也就是1時,表示情況安全,輸出為false,也就是0時,表示不安全情況發生。表4為這一安全約束下相關變量取值時,輸出res的真假情況。

表4 安全約束的相關變量真值

根據表4,對于提取的安全約束將通過數據流圖建模方式,構建為安全屬性模型,如圖8所示,按照同樣的流程,構建針對UCA2的安全屬性模型,如圖9所示。

圖8 針對UCA1的安全屬性模型

圖9 針對UCA2的安全屬性模型

4.3 安全屬性驗證

當安全屬性模型構建完成后,通過頂層操作符串聯場景模型和安全屬性模型,最后分析串聯之后的模型輸出。這種形式化的驗證方法可以證明在待測模型中,安全屬性在所有周期和場景下的正確性。如果模型有效,在檢測結果一欄會顯示為Valid;為Falsifiale時,則證明模型無效,SCADE將給出反例,可以通過單步測試或導入反例,以修改模型。

進站停車場景的形式化驗證模型如圖10所示,其中Package1::Operator1是初始狀態機模型的集合形式,Operator3是安全屬性觀察模型的集合形式,將相應的變量連接起來,觀測res輸出。

圖10 形式化驗證模型

通過SCADE內置的驗證器驗證,模型分析用時1 s,檢驗結果為Valid。表示進站停車場景模型滿足安全屬性的觀察模型,即該模型滿足“在進站停車場景中,列車緊急制動未緩解時,車載控制器不能發送開門信息”這一安全約束。驗證結果如圖11所示。針對UCA2的安全約束,也進行上述驗證。經過驗證,檢驗結果為Valid,證明模型符合上述安全約束需求。根據STAMP系統安全理論及STPA安全分析方法可知,當場景滿足安全約束時,證明對應的不安全控制行為沒有發生,也就不會引發對應的系統級危險。

圖11 模型驗證結果

5 結論

本文在STAMP理論和STPA方法的基礎上,結合安全狀態機形式化建模方法與模型檢驗技術,提出了一種全自動無人駕駛復雜運營場景安全驗證的方法,并以列車自動進站停車場景為例,對本文方法的可行性和有效性進行了驗證分析,對于提高全自動無人駕駛系統的安全性具有重要的研究意義和應用價值,得出如下研究結論。

(1)將STAMP系統安全理論與安全狀態機形式化建模方法結合,充分發揮兩者的優勢,在充分辨識復雜運營場景潛在危險的同時,還可以對場景進行形式化安全驗證。

(2)通過定義分層控制結構模型與安全狀態機模型間的基本轉換規則,能夠降低復雜運營場景安全狀態機模型建模的難度、保證系統安全分析模型與形式化模型間的一致性。

(3)在運營場景安全分析的基礎上構建的安全狀態機形式化模型滿足系統安全約束,在全自動無人駕駛系統安全設計和安全改進的過程中具有重要應用價值。