• 
    

    
    

      99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看

      ?

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

      2024-03-13 01:53:54馬牧云張亞東
      關(guān)鍵詞:控制結(jié)構(gòu)狀態(tài)機(jī)進(jìn)站

      馬牧云,張亞東,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ù)十個正常運(yùn)營場景和異常場景[3]。不同運(yùn)營場景下,全自動無人駕駛系統(tǒng)具有不同的交互主體、交互行為和控制邏輯,系統(tǒng)危險及致因具有較強(qiáng)的隱蔽性和復(fù)雜性,給運(yùn)營安全帶來了新的挑戰(zhàn)。如何驗證全自動無人駕駛復(fù)雜運(yùn)營場景下的系統(tǒng)安全性,已經(jīng)成為全自動無人駕駛技術(shù)迫切需要解決的關(guān)鍵問題之一。

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

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

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

      1.1 STAMP理論與STPA方法

      STAMP理論是基于系統(tǒng)理論和控制理論的事故致因模型。其中重要的3個要素是:安全約束、分層安全控制結(jié)構(gòu)和過程模型,安全約束作為3個要素中最基本的概念,需要被正確有效地執(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主動分析方法用于危險致因分析,通過分析開發(fā)過程中潛在的危險致因因素,達(dá)到消除或控制危險源的目的。這種方法將分析過程主要分為以下幾個步驟:分析系統(tǒng)級危險、構(gòu)建分層控制結(jié)構(gòu)模型、辨識不安全控制行為、分析危險致因因素、制定相應(yīng)的安全約束[14]。在STPA方法中,實(shí)施不安全的控制行為會導(dǎo)致系統(tǒng)進(jìn)入危險狀態(tài)。在識別不安全控制行為時,常用的有以下4種分類[15]:

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

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

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

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

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

      安全狀態(tài)機(jī)(SSM)是一種圖形化的建模語言,具有并發(fā)性、層次性和通信機(jī)制[16]。主要由狀態(tài)和遷移兩部分組成,有激活和未激活兩種狀態(tài)。遷移有兩種屬性,分別為條件和行為(也就是賦值語句),位于遷移線上的行為只在遷移觸發(fā)時執(zhí)行。位于狀態(tài)機(jī)內(nèi)部的行為,需要在該狀態(tài)激活的每一個周期執(zhí)行。狀態(tài)機(jī)要從當(dāng)前狀態(tài)遷移至下一個狀態(tài),需要同時滿足3個條件,一是當(dāng)前狀態(tài)處于激活態(tài),二是滿足遷移條件,三是需要滿足遷移的優(yōu)先級。一個操作符可以包含一個或多個狀態(tài)機(jī),狀態(tài)機(jī)之間可以是并行或者嵌套的關(guān)系。如圖1所示,該模型有兩個狀態(tài),其中加粗邊框為初始狀態(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è)計問題。

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

      安全狀態(tài)機(jī)的驗證環(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 場景安全驗證方法流程

      2.1 場景安全驗證方法流程

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

      圖2 總體驗證框架

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

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

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

      步驟3:危險致因分析及安全約束提取。針對潛在的危險,結(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)建可形式化驗證的安全狀態(tài)機(jī)模型。

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

      當(dāng)安全狀態(tài)機(jī)的一個狀態(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è)計方式的不同,將狀態(tài)機(jī)劃分為4種類型[22],分別如下。

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

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

      (3)嵌套SCADE文本設(shè)計的狀態(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è)計的SSM。

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

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

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

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

      進(jìn)站停車場景是全自動無人駕駛場景中正線運(yùn)營時的場景之一。當(dāng)列車確認(rèn)收到滿足進(jìn)站條件的移動授權(quán),站臺門關(guān)閉,緊急停車按鈕未按下,人員防護(hù)開關(guān)SPKS置于非防護(hù)位,這4個條件滿足時,列車可以進(jìn)站。在該場景中列車需要完成自動駕駛進(jìn)站精準(zhǔn)停車;欠標(biāo)或過標(biāo)時根據(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)活動的對象,主要是各個子系統(tǒng)及設(shè)備。主要的交互信息如圖4所示。

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

      場景主要流程說明如下。

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

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

      (3)當(dāng)確認(rèn)收到移動授權(quán),站臺門關(guān)閉,緊急停車按鈕未按下,人員防護(hù)開關(guān)SPKS置于非防護(hù)位,這4個條件滿足后,列車可以進(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)故障,則及時屏蔽相應(yīng)的車門。車載控制器VOBC向車門控制器發(fā)送開門信息,向計算機(jī)聯(lián)鎖系統(tǒng)CI發(fā)送站臺門打開信息。

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

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

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

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

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

      A2:列車追尾。

      A3:列車與障礙物相撞。

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

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

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

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

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

      根據(jù)對列車自動進(jìn)站停車場景流程的定義和分解,提取場景中擔(dān)任控制器、執(zhí)行器、被控過程的部分,在進(jìn)站停車場景中,主要的上層控制器為車載控制器、控制中心、區(qū)域控制器、計算機(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ī)建模與安全屬性驗證

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

      根據(jù)進(jìn)站停車場景流程以及提煉的主要建模步驟,首先確定安全狀態(tài)機(jī)模型的基本框架,同時充分考慮安全分析中提取的安全約束內(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ù)時序類、命令類或被控部分自身狀態(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)級危險H1為例,給出安全驗證的過程。由上述安全分析可知,STPA識別的針對H1的不安全控制行為如下。

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

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

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

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

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

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

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

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

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

      4.3 安全屬性驗證

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

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

      圖10 形式化驗證模型

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

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

      5 結(jié)論

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

      (1)將STAMP系統(tǒng)安全理論與安全狀態(tài)機(jī)形式化建模方法結(jié)合,充分發(fā)揮兩者的優(yōu)勢,在充分辨識復(fù)雜運(yùn)營場景潛在危險的同時,還可以對場景進(jì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ìn)的過程中具有重要應(yīng)用價值。

      猜你喜歡
      控制結(jié)構(gòu)狀態(tài)機(jī)進(jìn)站
      幾種防空導(dǎo)彈自動駕駛儀的研究分析
      航天控制(2020年4期)2020-09-03 10:46:16
      進(jìn)站口上下行載頻切換時引起ATP制動問題分析
      基于有限狀態(tài)機(jī)的交會對接飛行任務(wù)規(guī)劃方法
      基于ATO控制結(jié)構(gòu)的地鐵列車智慧節(jié)能技術(shù)
      春運(yùn)期間北京西站共有154.8萬人次刷臉進(jìn)站
      祖國(2018年6期)2018-06-27 10:27:26
      閱讀(科學(xué)探秘)(2018年8期)2018-05-14 10:06:29
      SIL定量計算評估方法在BPCS中的應(yīng)用
      生成語法中的控制結(jié)構(gòu)研究述評
      重慶軌道交通三號線列車進(jìn)站警示功能接口電路的分析
      FPGA設(shè)計中狀態(tài)機(jī)安全性研究
      邵阳县| 浮梁县| 友谊县| 惠水县| 长沙市| 酉阳| 固原市| 芦溪县| 宜兰市| 上高县| 当雄县| 新巴尔虎左旗| 洛浦县| 顺平县| 邹城市| 天全县| 富平县| 阜新| 渭南市| 札达县| 礼泉县| 台东市| 连云港市| 青州市| 郯城县| 阿荣旗| 武邑县| 阳原县| 沙坪坝区| 盐边县| 黄梅县| 井冈山市| 阜阳市| 云和县| 秭归县| 金湖县| 轮台县| 惠东县| 奉贤区| 新绛县| 简阳市|