馬牧云，張亞東，2，李 耀，郭 進(jìn)，2

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

引言

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

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

本文基于STAMP系統(tǒng)安全分析理論,引入安全狀態(tài)機(jī)建模方法,提出了一種基于STAMP理論與模型檢驗(yàn)相結(jié)合的復(fù)雜運(yùn)營場景安全驗(yàn)證方法。

1 安全分析及驗(yàn)證理論基礎(chǔ)

1.1 STAMP理論與STPA方法

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

(1)未提供控制行為導(dǎo)致危險(xiǎn);

(2)提供錯(cuò)誤的控制行為導(dǎo)致危險(xiǎn);

(3)提供控制行為的時(shí)間過早或過晚導(dǎo)致危險(xiǎn);

(4)控制行為作用的時(shí)間過長或過短導(dǎo)致危險(xiǎn)。

1.2 安全狀態(tài)機(jī)建模與模型檢驗(yàn)方法

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

圖1 基礎(chǔ)安全狀態(tài)機(jī)模型

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

2 場景安全驗(yàn)證方法流程

2.1 場景安全驗(yàn)證方法流程

基于STAMP理論與模型檢驗(yàn)的復(fù)雜運(yùn)營場景安全驗(yàn)證框架主要包括三部分:基于STAMP理論和STPA方法的運(yùn)營場景安全分析、運(yùn)營場景安全狀態(tài)機(jī)形式化模型的構(gòu)建、運(yùn)營場景的形式化安全驗(yàn)證?？傮w驗(yàn)證框架如圖2所示。

圖2 總體驗(yàn)證框架

本文的驗(yàn)證過程主要分為以下5個(gè)步驟。

步驟1:運(yùn)營場景分層控制結(jié)構(gòu)模型的構(gòu)建。針對具體運(yùn)營場景,首先確定可能發(fā)生的系統(tǒng)級事故及危險(xiǎn),提取運(yùn)營場景中涉及到的控制器、執(zhí)行器、傳感器、被控過程以及交互信息等建模要素,遵循分層控制結(jié)構(gòu)模型自上而下的建模順序,確定頂層控制器,并根據(jù)各個(gè)組件的信息交互行為,逐級構(gòu)建運(yùn)營場景的分層控制結(jié)構(gòu)模型。以便后續(xù)分析導(dǎo)致系統(tǒng)層面危險(xiǎn)發(fā)生的致因因素。

步驟2:辨識導(dǎo)致危險(xiǎn)發(fā)生的不安全控制行為。分層控制結(jié)構(gòu)模型表現(xiàn)了系統(tǒng)或場景中控制器和執(zhí)行器的控制行為,結(jié)合分層控制結(jié)構(gòu)模型以及相關(guān)場景規(guī)范,通過上述4種不恰當(dāng)控制行為的分類,辨識場景中的不安全控制行為。

步驟3:危險(xiǎn)致因分析及安全約束提取。針對潛在的危險(xiǎn),結(jié)合分層控制結(jié)構(gòu)模型,構(gòu)建過程模型細(xì)化分析,確定導(dǎo)致不安全控制行為發(fā)生的致因因素,并提取相應(yīng)的安全約束。

步驟4:運(yùn)營場景安全狀態(tài)機(jī)建模。通過提取運(yùn)營場景分層控制結(jié)構(gòu)模型中的模型要素,基于分層控制結(jié)構(gòu)模型與安全狀態(tài)機(jī)模型之間的轉(zhuǎn)換規(guī)則,充分考慮運(yùn)營場景安全約束,利用安全狀態(tài)機(jī)建模方法,在SCADE環(huán)境中,構(gòu)建可形式化驗(yàn)證的安全狀態(tài)機(jī)模型。

步驟5:運(yùn)營場景安全驗(yàn)證。利用數(shù)據(jù)流圖建模方法,針對提取的運(yùn)營場景安全約束,構(gòu)建相應(yīng)的安全屬性模型,通過SCADE形式化工具,結(jié)合模型檢驗(yàn)技術(shù),對運(yùn)營場景下的安全狀態(tài)機(jī)模型進(jìn)行形式化安全驗(yàn)證。

2.2 分層控制結(jié)構(gòu)模型與安全狀態(tài)機(jī)模型間轉(zhuǎn)換規(guī)則

根據(jù)分層控制結(jié)構(gòu)模型與安全狀態(tài)機(jī)模型的定義和特點(diǎn),給出了兩種模型之間的基本轉(zhuǎn)換規(guī)則定義。在構(gòu)建的過程中,變量的名稱可以根據(jù)實(shí)際所需要的內(nèi)容自行定義,結(jié)合實(shí)際設(shè)計(jì)方式進(jìn)行擴(kuò)展。

當(dāng)安全狀態(tài)機(jī)的一個(gè)狀態(tài)創(chuàng)建完成后,需要對其屬性進(jìn)行設(shè)置,通常包括狀態(tài)機(jī)名稱、起始狀態(tài)以及終止?fàn)顟B(tài)等。轉(zhuǎn)換過程的第一步需要根據(jù)狀態(tài)機(jī)的狀態(tài)內(nèi)行為設(shè)計(jì)方式的不同,將狀態(tài)機(jī)劃分為4種類型[22],分別如下。

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

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

(3)嵌套SCADE文本設(shè)計(jì)的狀態(tài)機(jī),用于控制行為便于用SCADE文本表達(dá)的情況。

(4)隱藏文本內(nèi)容的狀態(tài)機(jī),用于行為元素?zé)o法被狀態(tài)布局容納的情況下。

分層控制結(jié)構(gòu)模型能夠表現(xiàn)待分析系統(tǒng)或場景中交互主體的通信關(guān)系、信息交互內(nèi)容等。其核心結(jié)構(gòu)有控制器、執(zhí)行器、傳感器、被控過程等?；诖?定義以下規(guī)則,模型轉(zhuǎn)換基本原則如圖3所示。

圖3 模型轉(zhuǎn)換規(guī)則示意

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

規(guī)則2:系統(tǒng)中執(zhí)行器需要發(fā)送信息至下一級控制器或自身狀態(tài)需要根據(jù)接收到的命令改變,針對執(zhí)行器的行為邏輯結(jié)合實(shí)際場景,將其構(gòu)建為嵌套SCADE文本的SSM或嵌套基于模型設(shè)計(jì)的SSM。

規(guī)則3:傳感器作為兩層控制器之間的信息反饋裝置,根據(jù)需要反饋的信息類型,結(jié)合實(shí)際場景構(gòu)建為無行為邏輯的SSM或嵌套基于模型設(shè)計(jì)的SSM。

規(guī)則4:被控過程構(gòu)建為無行為邏輯的SSM。

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

3 列車自動進(jìn)站停車場景安全分析

進(jìn)站停車場景是全自動無人駕駛場景中正線運(yùn)營時(shí)的場景之一。當(dāng)列車確認(rèn)收到滿足進(jìn)站條件的移動授權(quán),站臺門關(guān)閉,緊急停車按鈕未按下,人員防護(hù)開關(guān)SPKS置于非防護(hù)位,這4個(gè)條件滿足時(shí),列車可以進(jìn)站。在該場景中列車需要完成自動駕駛進(jìn)站精準(zhǔn)停車;欠標(biāo)或過標(biāo)時(shí)根據(jù)距離的不同,設(shè)置不同的運(yùn)行模式最終對標(biāo)停車;安全打開站臺門及車門,確保車門與站臺門對位隔離,對應(yīng)打開或關(guān)閉。

3.1 列車自動進(jìn)站停車場景描述

根據(jù)相關(guān)技術(shù)規(guī)范,對列車進(jìn)站停車場景進(jìn)行描述[23-24]。該流程包括參加系統(tǒng)活動的對象,主要是各個(gè)子系統(tǒng)及設(shè)備。主要的交互信息如圖4所示。

圖4 進(jìn)站停車場景活動圖

場景主要流程說明如下。

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

(2)車載控制器VOBC確認(rèn)線路信息并發(fā)送列車相關(guān)信息至區(qū)域控制器ZC,ZC需確認(rèn)收到并根據(jù)信息計(jì)算移動授權(quán)MA。

(3)當(dāng)確認(rèn)收到移動授權(quán),站臺門關(guān)閉,緊急停車按鈕未按下,人員防護(hù)開關(guān)SPKS置于非防護(hù)位,這4個(gè)條件滿足后,列車可以進(jìn)站停車。

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

(5)判斷車輛速度為0后,判斷站臺門是否發(fā)生故障,若發(fā)現(xiàn)故障,則及時(shí)屏蔽相應(yīng)的車門。車載控制器VOBC向車門控制器發(fā)送開門信息,向計(jì)算機(jī)聯(lián)鎖系統(tǒng)CI發(fā)送站臺門打開信息。

(6)車門控制器收到信息并打開車門,確認(rèn)狀態(tài),向車載控制器VOBC反饋信息;同時(shí)計(jì)算機(jī)聯(lián)鎖系統(tǒng)發(fā)送開門信息至站臺門控制器,站臺門控制器收到信息打開站臺門并確認(rèn)狀態(tài),反饋至計(jì)算機(jī)聯(lián)鎖系統(tǒng)。

(7)控制中心向站臺廣播系統(tǒng)發(fā)送信息,站臺廣播進(jìn)行播報(bào)。

3.2 列車進(jìn)站停車危險(xiǎn)分析

根據(jù)進(jìn)站停車場景分析,可能發(fā)生的系統(tǒng)級事故如下。

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

A2:列車追尾。

A3:列車與障礙物相撞。

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

針對上述三類事故,給出在進(jìn)站停車場景中的系統(tǒng)級危險(xiǎn)如下。

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

H2:列車進(jìn)站時(shí)超速(可能導(dǎo)致A2、A3)。

3.3 系統(tǒng)分層控制結(jié)構(gòu)模型

根據(jù)對列車自動進(jìn)站停車場景流程的定義和分解,提取場景中擔(dān)任控制器、執(zhí)行器、被控過程的部分,在進(jìn)站停車場景中,主要的上層控制器為車載控制器、控制中心、區(qū)域控制器、計(jì)算機(jī)聯(lián)鎖。各控制器需要發(fā)送相關(guān)指令或場景所需要的信息至下一層結(jié)構(gòu)。車門控制器及站臺門控制器擔(dān)任執(zhí)行器的作用,處理上層控制器發(fā)送的命令并對下一層的控制器或執(zhí)行器發(fā)出指令。車門、站臺門及列車根據(jù)實(shí)際場景需求,提取為被控過程進(jìn)行建模。構(gòu)建完成的分層控制結(jié)構(gòu)模型如圖5所示。

圖5 進(jìn)站停車分層控制結(jié)構(gòu)模型

3.4 不安全控制行為

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

表1 部分不安全控制行為辨識結(jié)果

3.5 致因分析

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

表2 部分致因分析結(jié)果及安全約束

圖6 車門控制過程模型

4 列車自動進(jìn)站停車場景的安全狀態(tài)機(jī)建模與安全屬性驗(yàn)證

4.1 進(jìn)站停車場景的安全狀態(tài)機(jī)模型

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

表3 部分變量類型及含義

圖7 進(jìn)站停車場景的安全狀態(tài)機(jī)模型

4.2 安全屬性模型構(gòu)建

以系統(tǒng)級危險(xiǎn)H1為例,給出安全驗(yàn)證的過程。由上述安全分析可知,STPA識別的針對H1的不安全控制行為如下。

UCA1:緊急制動未緩解時(shí)車門開啟。

UCA2:站臺門發(fā)生故障時(shí)未隔離相應(yīng)車門。

由于緊急制動未緩解,在該場景中是因?yàn)榱熊嚽?過標(biāo)5 m以上導(dǎo)致的,此時(shí)并未申請人工救援,列車不處于安全停車范圍內(nèi),如果此時(shí)打開車門將會導(dǎo)致危險(xiǎn)。

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

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

表4 安全約束的相關(guān)變量真值

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

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

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

4.3 安全屬性驗(yàn)證

當(dāng)安全屬性模型構(gòu)建完成后,通過頂層操作符串聯(lián)場景模型和安全屬性模型,最后分析串聯(lián)之后的模型輸出。這種形式化的驗(yàn)證方法可以證明在待測模型中,安全屬性在所有周期和場景下的正確性。如果模型有效,在檢測結(jié)果一欄會顯示為Valid;為Falsifiale時(shí),則證明模型無效,SCADE將給出反例,可以通過單步測試或?qū)敕蠢?以修改模型。

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

圖10 形式化驗(yàn)證模型

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

圖11 模型驗(yàn)證結(jié)果

5 結(jié)論

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

(1)將STAMP系統(tǒng)安全理論與安全狀態(tài)機(jī)形式化建模方法結(jié)合,充分發(fā)揮兩者的優(yōu)勢,在充分辨識復(fù)雜運(yùn)營場景潛在危險(xiǎn)的同時(shí),還可以對場景進(jìn)行形式化安全驗(yàn)證。

(2)通過定義分層控制結(jié)構(gòu)模型與安全狀態(tài)機(jī)模型間的基本轉(zhuǎn)換規(guī)則,能夠降低復(fù)雜運(yùn)營場景安全狀態(tài)機(jī)模型建模的難度、保證系統(tǒng)安全分析模型與形式化模型間的一致性。

(3)在運(yùn)營場景安全分析的基礎(chǔ)上構(gòu)建的安全狀態(tài)機(jī)形式化模型滿足系統(tǒng)安全約束,在全自動無人駕駛系統(tǒng)安全設(shè)計(jì)和安全改進(jìn)的過程中具有重要應(yīng)用價(jià)值。