石夢燁，胡 軍，陳 朔，唐紅英，王立松

(南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，南京 211106)(軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心，南京 211106)

1 引 言

近年來，隨著各類安全關(guān)鍵系統(tǒng)[1，2]功能的不斷增強(qiáng)和需求的日益增加，對傳統(tǒng)的系統(tǒng)工程開發(fā)和安全性分析技術(shù)提出了很大的挑戰(zhàn).基于模型的安全性分析[3，4](Model Based Safety Analysis，MBSA)是近年出現(xiàn)的一類對復(fù)雜系統(tǒng)建模并基于系統(tǒng)模型實現(xiàn)自動或半自動化的安全分析及驗證的技術(shù)方法.MBSA已成為系統(tǒng)建模和分析領(lǐng)域的一個熱點研究問題.

MBSA方法是形式化方法在安全關(guān)鍵系統(tǒng)的應(yīng)用，旨在系統(tǒng)復(fù)雜性上升的同時保持或提高其安全性水平.它用于支持系統(tǒng)設(shè)計層級的分析，包括三個關(guān)鍵要素[5]：

1)對整個系統(tǒng)進(jìn)行形式化模型的構(gòu)建，其中模型是組件的集合；

2)對模型進(jìn)行定性和定量分析，將可能存在的安全問題設(shè)置成一系列故障模式；

3)對擴(kuò)展模型進(jìn)行形式化安全分析.

國際汽車工程師協(xié)會(Society of Automotive Engineers，SAE)架構(gòu)分析與設(shè)計語言(Architecture Analysis and Design Language，AADL)[6，7]是一種形式化建模語言，通過可擴(kuò)展的標(biāo)記符、工具框架和精確的語法語義，用于設(shè)計和分析復(fù)雜系統(tǒng)的軟件和硬件架構(gòu)及其性能關(guān)鍵特性.

本文主要工作以AADL的子集SLIM為建模語言，基于xSAP(The eXtended Safety Assessment Platform)為安全性分析平臺的形式化驗證方法[8]，以AIR6110中的機(jī)輪剎車系統(tǒng)[9]為實例，對其進(jìn)行安全性建模和分析.通過一個實例展現(xiàn)了面向SLIM模型進(jìn)行安全性分析和形式化驗證的過程.本文的結(jié)構(gòu)安排如下：第二節(jié)，主要介紹了MBSA框架、形式化方法在MBSA的應(yīng)用、建模語言SLIM，和驗證工具NuSMV[10，11]；第三節(jié)，簡要介紹了AIR6110標(biāo)準(zhǔn)和機(jī)輪剎車系統(tǒng)，并詳細(xì)給出了用SLIM對其進(jìn)行形式化建模的過程以及建模時遇到的問題，設(shè)計了多種類的故障模式并進(jìn)行模型擴(kuò)展；第四節(jié)對建立的機(jī)輪剎車模型進(jìn)行分析并展現(xiàn)了驗證結(jié)果；最后總結(jié)全文.

2 基于形式化方法的安全性分析方法架構(gòu)

2.1 MBSA框架

MBSA方法學(xué)是一種系統(tǒng)設(shè)計工程師和安全工程師共享使用基于模型的開發(fā)過程創(chuàng)建的公共系統(tǒng)模型的方法[12].如圖1所示，在設(shè)計階段通過形式化語言描述復(fù)雜系統(tǒng)的行為架構(gòu)，來構(gòu)造一個通用的需求模型；在安全性分析階段中基于所建立的系統(tǒng)模型來進(jìn)行失效行為的語義擴(kuò)展，并盡可能的自動化生成系統(tǒng)失效行為的最小割集故障樹[13]和失效序列.

圖1 MBSA方法框架Fig.1 MBSA method framework

總體上來看，MBSA的總目標(biāo)是：1)提供一個可公用且嚴(yán)格定義的系統(tǒng)模型，確保隨著系統(tǒng)架構(gòu)的發(fā)展，安全分析結(jié)果是最新的；2)通過將傳統(tǒng)的安全分析過程與基于模型的開發(fā)活動相結(jié)合，允許開發(fā)早期可以進(jìn)行安全評估，降低因系統(tǒng)復(fù)雜度提高造成的成本增加并提高安全分析過程的質(zhì)量；3)系統(tǒng)開發(fā)工程師和系統(tǒng)安全工程師可以通過公用的形式化模型進(jìn)行溝通，便于對系統(tǒng)的理解.

2.2 MBSA中的形式化方法

形式化方法[5，14]是將數(shù)理和邏輯方法(如邏輯、自動機(jī)、圖論)運(yùn)用在計算機(jī)工程領(lǐng)域，通過借助形式化語言，去構(gòu)建計算機(jī)系統(tǒng)的數(shù)學(xué)模型并進(jìn)行模型推理和驗證.它的應(yīng)用領(lǐng)域是多方面的：首先使用形式化語言去描述符合語法語義規(guī)則的完整的系統(tǒng)模型；其次使用形式化分析技術(shù)和形式化工具分析系統(tǒng)模型；最后，形式化方法滲透在系統(tǒng)開發(fā)過程的各個階段，包括需求分析、設(shè)計、實現(xiàn).它可以用來引導(dǎo)安全關(guān)鍵系統(tǒng)的開發(fā)過程，盡早發(fā)現(xiàn)每個階段的缺陷問題.

在系統(tǒng)的開發(fā)過程中，采用具有嚴(yán)格語法語義定義的形式化建模語言可以建立精確且公用的數(shù)學(xué)模型.在安全評估過程中，采用形式化分析技術(shù)可以對公用的系統(tǒng)模型的擴(kuò)展形式進(jìn)行分析和驗證，來發(fā)現(xiàn)模型中可能存在的安全問題.采用形式化工具可以自動化驗證過程，減少人工檢查的高成本并減少錯誤.因此形式化方法在MBSA方法中極為重要[15，16].

MBSA的起點和重點是創(chuàng)建公用的需求模型.在本文工作中選用的是系統(tǒng)級集成建模語言(System-Level Integrated Modeling language，SLIM)對系統(tǒng)進(jìn)行需求規(guī)約.SLIM是AADL的精化，一個完整的SLIM系統(tǒng)規(guī)范由三部分組成，即正常行為的描述、錯誤行為的描述以及描述錯誤行為如何影響正常行為的故障注入規(guī)范.NuSMV(New Symbolic Model Verifier)是一個符號模型檢驗工具，支持先進(jìn)的模型檢驗技術(shù)[17]，基于BDD(Binary Decision Diagrams)和SAT(Satisfiability)針對CTL(Computation Tree Logic)[10]和LTL(Linear Temporal Logic)[18]時態(tài)邏輯進(jìn)行驗證，可用于對SLIM建立的需求模型進(jìn)行分析.

3 AIR6110標(biāo)準(zhǔn)中的機(jī)輪剎車系統(tǒng)的實例建模研究

3.1 AIR6110標(biāo)準(zhǔn)和WBS概述

在本文的工作中，選擇了在SAE的AIR6110標(biāo)準(zhǔn)中所給出的一個典型的安全關(guān)鍵系統(tǒng)實例展開研究，這是一個航空領(lǐng)域中的飛機(jī)機(jī)輪剎車系統(tǒng)的系統(tǒng)規(guī)范和安全性分析實例.AIR6110文件由SAE于2011年發(fā)布，SAE AIR6110的全稱是“連續(xù)飛機(jī)/系統(tǒng)開發(fā)過程示例”，其中機(jī)輪剎車系統(tǒng)(WBS)的開發(fā)和安全性分析完全遵循工業(yè)標(biāo)準(zhǔn)ARP4754A—“民用飛機(jī)和系統(tǒng)發(fā)展指南”[19]和ARP47611—“進(jìn)行民用機(jī)載系統(tǒng)和設(shè)備安全評估程序的指南和方法”[20]中的要求.ARP4754和ARP4761是目前航空電子領(lǐng)域的開發(fā)和安全評估過程的工業(yè)標(biāo)準(zhǔn).

圖2 機(jī)輪剎車系統(tǒng)模型概觀Fig.2 Overview of the wheel brake system model

在AIR6110所給出的這個實例系統(tǒng)中，主要描述了WBS的系統(tǒng)框架結(jié)構(gòu)和功能要求，其中，WBS由制動系統(tǒng)控制單元(Brake System Control System，BSCU)和液壓調(diào)節(jié)系統(tǒng)組成.圖2是機(jī)輪剎車系統(tǒng)的模型概觀.

BSCU是系統(tǒng)中的數(shù)據(jù)處理組件，收集來自踏板、機(jī)輪速度等信息作為輸入，使用內(nèi)部的命令單元進(jìn)行計算并向液壓調(diào)節(jié)系統(tǒng)輸出不同命令：傳輸?shù)揭簤赫{(diào)節(jié)系統(tǒng)正常線路的控制命令，傳輸?shù)揭簤赫{(diào)節(jié)系統(tǒng)備用線路的控制命令，對關(guān)閉閥和選擇閥進(jìn)行調(diào)控的開關(guān)命令.BSCU還包含監(jiān)控單元，主要用于監(jiān)控命令單元的狀態(tài).默認(rèn)情況下，BSCU使用第一組命令和監(jiān)控設(shè)備.當(dāng)監(jiān)控設(shè)備發(fā)出錯誤警報，則由選擇設(shè)備自動切換成備用組.

液壓調(diào)節(jié)系統(tǒng)用于對機(jī)輪進(jìn)行供壓，分為正常線路和備用線路.正常線路包括綠色液壓泵、關(guān)閉閥、限量閥；備用線路包括藍(lán)色液壓泵、隔離閥、蓄壓泵、防滑閥、人工剎車裝置.正常線路由綠色液壓泵供壓，備用線路處于待機(jī)狀態(tài)，由藍(lán)色液壓泵供壓.當(dāng)藍(lán)色液壓泵失效時，由用于驅(qū)動剎車制動器的蓄壓泵支持.選擇閥為兩條線路共有，起線路切換功能.當(dāng)正常線路失效，則轉(zhuǎn)換至備用線路.若備用線路也失效，則由人工剎車裝置額外提供液壓.

3.2 WBS的形式化建模

上一節(jié)用自然語言概要描述了AIR6110標(biāo)準(zhǔn)中的WBS系統(tǒng)架構(gòu)和功能，接下來在本節(jié)中將采用SLIM對WBS系統(tǒng)的功能進(jìn)行形式化建模.本文將機(jī)輪剎車系統(tǒng)按表1所示分層結(jié)構(gòu)建模.

表1 WBS分層模型整體框架圖
Table 1 Overall framework of WBS hierarchical model

模型層級系統(tǒng)包含的子組件BSCU子系統(tǒng)第一層WBS液壓調(diào)節(jié)系統(tǒng)監(jiān)控器lru1、第二層BSCU子系統(tǒng)lru2、選擇設(shè)備綠色液壓泵、藍(lán)色液壓泵、第二層液壓調(diào)節(jié)系統(tǒng)關(guān)閉閥、蓄壓泵、隔離閥、選擇閥、限量閥、防滑閥、人工剎車裝置第三層LRU監(jiān)控單元命令單元

給出液壓調(diào)節(jié)系統(tǒng)的選擇閥的SLIM描述如圖3所示，其他部件可以通過類似方法得到其對應(yīng)的SLIM代碼模塊，在此不再贅述.

首先設(shè)置端口，選擇閥的輸入端口有來自蓄壓泵的液壓accumulator_input，來自正常線路的液壓green_input，來自備用線路的液壓blue_input，來自monitor的事件switch，以及來自BSCU的select_alternate.輸出端口有g(shù)reen_out，blue_out.其中，accumulator_input、green_input和blue_input的數(shù)據(jù)類型是intRange，范圍是[0…10]，初始值為5，select_alternate是布爾型端口，初始值為false.

共設(shè)置四種模式：select_green、select_blue、select_accu、fail，初始模式是select_green.圖3設(shè)置了7種轉(zhuǎn)換.

第1個轉(zhuǎn)換說明，如果收到的數(shù)據(jù)端口綠色液壓值大于等于5，則說明使用正常線路，那么令液壓值等于輸入的綠色液壓值.

圖3 選擇閥建模代碼
Fig.3 Selector modeling

第2、3、4這三個轉(zhuǎn)換說明如果收到的綠色液壓值green_input小于5，則選擇備用線路；收到switch事件，則系統(tǒng)從select_green轉(zhuǎn)變?yōu)閟elect_blue，即選擇備用線路；當(dāng)選擇閥收到來自BSCU的select_alterate值為true，即表示當(dāng)前正常線路出現(xiàn)了問題，則使用備用線路，令選擇閥的輸出液壓值為藍(lán)色液壓值.

第5、6、7這三個轉(zhuǎn)換說明，如果收到的來自藍(lán)色液壓泵的液壓值≥5，則使用備用線路，并令選擇閥的輸出液壓值為藍(lán)色液壓值；若收到的藍(lán)色液壓值<5，而蓄壓泵的液壓值≥5，則使用蓄壓泵的液壓值；當(dāng)蓄壓泵的液壓值也小于5，說明蓄壓泵也出現(xiàn)問題，則失敗.

在面對AIR6110標(biāo)準(zhǔn)建模的過程中，我們發(fā)現(xiàn)了一些在AIR6110標(biāo)準(zhǔn)文檔中尚未清楚闡述的地方，如：在標(biāo)準(zhǔn)的文字描述中給出“正常線路的液壓值會作為反饋傳輸?shù)紹SCU中.當(dāng)該反饋值小于指定的值時，就類似于一個指示信號，指示正常線路失效.這種情況下，BSCU會產(chǎn)生一個命令，將關(guān)閉閥關(guān)閉.”并未說明BSCU的命令如何傳到該閥？此外，AIR6110標(biāo)準(zhǔn)中的Arch4架構(gòu)顯示，監(jiān)控單元有一根連著關(guān)閉閥的線，它是否可以用來控制閥門?

由此可見，自然語言存在無法闡述清楚系統(tǒng)需求或者存在二義性問題.而形式化方法是基于形式化語言的，具有非常精確的語義，因此可以明確地解釋系統(tǒng)出現(xiàn)的問題.在進(jìn)行形式化建模的時候，新的系統(tǒng)除去了由液壓調(diào)節(jié)系統(tǒng)指向BSCU的液壓反饋值.建模時，在BSCU系統(tǒng)中單獨建了一個select系統(tǒng)，它接受來自于監(jiān)控單元的數(shù)據(jù)，用于判斷是否使用備用液壓，它的輸出select_alternate會傳到關(guān)閉閥中.如果select_alternate為true，則說明當(dāng)前正常線路出現(xiàn)了問題，那么則關(guān)閉關(guān)閉閥.

另外，在標(biāo)準(zhǔn)文字表達(dá)中出現(xiàn)：“防滑閥也能對液壓進(jìn)行調(diào)整”，實際系統(tǒng)中如何體現(xiàn)對液壓的修改？

由于標(biāo)準(zhǔn)中記載的防滑閥和限量閥的功能是：“防滑閥遵循BSCU傳出的命令去控制制動器的液壓，它用于限制制動器的液壓管路壓力以防止機(jī)輪鎖定.”以及“當(dāng)飛行員或自動剎車系統(tǒng)測量到壓力超過滑行輪胎所需的壓力時，通過降低制動壓力來優(yōu)化制動.限量閥根據(jù)BSCU傳來的控制命令，對液壓調(diào)節(jié)系統(tǒng)的液壓值進(jìn)行調(diào)節(jié)，并把調(diào)節(jié)后的值傳輸?shù)綑C(jī)輪.”也就是說，防滑閥和限量閥的主要功能是降低制動壓力.所以，在使用SLIM進(jìn)行建模的時候，設(shè)置它們的壓力變化為不變和下降.相應(yīng)的，BSCU產(chǎn)生的命令為down和nochange.

3.3 用xSAP對WBS模型故障擴(kuò)展

由于上一節(jié)中建立的模型是假設(shè)系統(tǒng)在理想情況下運(yùn)行.而實際情況下，安全分析需要考慮到可能發(fā)生的不同故障以及系統(tǒng)組件可能出現(xiàn)故障的各種方式，因此必須使用系統(tǒng)的故障行為來增強(qiáng)基于模型的開發(fā)中捕獲的正常系統(tǒng)行為.xSAP支持基于庫的故障模式定義，可以對正常的系統(tǒng)功能行為進(jìn)行模型擴(kuò)展，擴(kuò)展后的模型通過安全性分析來評估存在故障的系統(tǒng)行為.

3.3.1 故障設(shè)置

在此以液壓調(diào)節(jié)系統(tǒng)中的閥類為例設(shè)計故障.對關(guān)閉閥設(shè)置了三種不同的狀態(tài)：OK，Dead，Stuck_at_zero.OK表示初始狀態(tài)，Dead是失效狀態(tài)，失效的原因來自于內(nèi)部軟件錯誤事件internal_error.Stuck_at_zero是卡死狀態(tài)，當(dāng)出現(xiàn)錯誤事件stuck_at_zero時，pump會從OK變成Stuck_at_zero.這種情況下，無論輸入的液壓值是多少，輸出的液壓值都為0.

具體實現(xiàn)中，設(shè)置兩個故障事件，internal_error和stuck_at_zero.internal_error是液壓錯誤事件，stuck_at_zero是卡死故障，表示卡死在液壓值0.接下來定義轉(zhuǎn)換，分別定義了以下轉(zhuǎn)換：

1)OK-[Internal_error]->Dead；

2)OK-[stuck_at_zero]->Stuck_at_zero.

系統(tǒng)初始時處于OK狀態(tài)，當(dāng)遇到故障事件internal_error，會從OK轉(zhuǎn)為Dead.當(dāng)遇到卡死事件stuck_at_zero，會從OK轉(zhuǎn)為Stuck_at_zero.

3.3.2 故障擴(kuò)展

上一節(jié)中所設(shè)計的系統(tǒng)故障行為是從安全性分析的視角來進(jìn)行設(shè)計的，還需要進(jìn)一步將這些可能的故障信息與正常的系統(tǒng)功能行為合并在同一個模型中進(jìn)行完整的系統(tǒng)分析.這種合并是通過在模型層的故障注入方式來實現(xiàn)的.

故障注入描述了錯誤發(fā)生對系統(tǒng)正常行為的影響.更具體地說，它指定當(dāng)關(guān)聯(lián)的錯誤模型進(jìn)入特定錯誤狀態(tài)時組件實現(xiàn)中的數(shù)據(jù)元素經(jīng)歷的值更新.

在本實例的研究中使用xSAP對模型進(jìn)行擴(kuò)展，選擇三個故障注入，分別是:1)電源2發(fā)生故障；2)主模式BSCU系統(tǒng)中的監(jiān)控單元出現(xiàn)錯誤；3)液壓調(diào)節(jié)系統(tǒng)中的綠色液壓泵發(fā)生錯誤.

4 機(jī)輪剎車模型的安全性分析

形式化分析工具可以用來對建立的模型進(jìn)行安全性分析.以xSAP為核心的COMPASS(Correctness，Modeling，and Performance of Aerospace Systems)分析[21，22]包括對系統(tǒng)進(jìn)行形式化建模，即建立SLIM模型；對系統(tǒng)進(jìn)行定性分析并設(shè)計安全屬性；考慮系統(tǒng)可能存在的失效行為并進(jìn)行語義擴(kuò)展和分析.COMPASS的輸入為根據(jù)系統(tǒng)架構(gòu)建立的正常模型和設(shè)置的故障模式，以及一組表示系統(tǒng)規(guī)約的屬性.輸出為反例路徑、故障樹、FMEA表[5，23]、FDIR[24]等可視化界面.

4.1 模型的動態(tài)仿真

模型模擬主要用于檢查系統(tǒng)功能的正確性.圖4是模型的部分運(yùn)行圖形，在此選擇運(yùn)行的步長為20.軌跡由一個表格組成，其中第一列提供了模型元素的名稱，在其他列中顯示了該元素在每個步驟的值.布爾條紋顯示為具有兩個值的波形，其中high為true，low為false.

圖4 對擴(kuò)展的WBS系統(tǒng)進(jìn)行動態(tài)仿真Fig.4 Dynamic simulation of extended WBS systems

通過圖4中的模擬結(jié)果可以發(fā)現(xiàn)，由于主模式的監(jiān)控單元發(fā)生了invalidReport錯誤，導(dǎo)致判斷監(jiān)控單元是否有效的輸出valid的值為false，該故障作為故障傳播進(jìn)入BSCU中的select_Alternate.監(jiān)控器收到來自BSCU中監(jiān)控器的錯誤，引發(fā)switch事件，switchBSCU和alarmBSCU變?yōu)閠rue，switch事件傳入BSCU，導(dǎo)致BSCU系統(tǒng)從Primary轉(zhuǎn)為Backup.

4.2 模型檢測

模型檢測用于根據(jù)一個或多個屬性檢查SLIM模型.通過將指定的屬性描述為時態(tài)邏輯公式并使用特定的符號算法進(jìn)行狀態(tài)空間的智能搜索來確定屬性是真是假.若屬性為假，則生成反例軌跡以顯示違反該屬性的模型的執(zhí)行軌跡來進(jìn)行深入的進(jìn)一步分析.否則，顯示屬性正確.共設(shè)計并驗證了15條屬性，其中6條正確，9條錯誤，耗時8.36秒.

圖5 模型檢查得到錯誤屬性的反例Fig.5 Model check gets a counterexample of the wrong attribute

在此選取其中兩個進(jìn)行說明.首先對屬性“AG(valid=false and bscu.mode=mode：Backup-> AF alarmBSCU)has been found false.”進(jìn)行驗證，該屬性的含義為：無論何時原子命題“valid=false and bscu.mode=mode：Backup”成立，它最終一定會被響應(yīng)alarmBSCU.如圖5所示，結(jié)果顯示該CTL屬性錯誤并給出反例路徑.

接下來對CTL屬性“AG(bscu.mode=mode：Backup and bscu.valid=false-> EF alarmBSCU)has been found true”進(jìn)行檢查，它的含義是當(dāng)BSCU當(dāng)前的模式是Backup，并且valid值為false，則表明BSCU系統(tǒng)已經(jīng)是失效，可能會響應(yīng)警報alarmBSCU.在模型中，該CTL屬性成立.

4.3 形式化模型的安全性分析

經(jīng)典的系統(tǒng)安全性分析方法有故障樹分析(Fault Tree Analysis，F(xiàn)TA)和故障模式和影響分析(Fault Mode and Effect Analysis，F(xiàn)MEA).FTA是一種自頂向下的方法，它通過考慮所分析系統(tǒng)的意外行為，自上而下分析追蹤直到找出所有故障模式.FMEA則是一種自底向上的方法，它通過考慮給定的危害的起因，分析其可能的安全后果.

4.3.1 故障樹分析

在此選擇屬性“bscu fail twice”作為頂層故障事件(Top Level Event，TLE)進(jìn)行故障樹分析的說明，它的不定式是“bscu.valid=false and bscu.mode=Backup”，含義是當(dāng)前BSCU子系統(tǒng)處于備用模式且輸出端口valid的值為false，即兩個監(jiān)控命令單元都失效.這種情況下，說明整個BSCU子系統(tǒng)已經(jīng)失效.使用COMPASS中生成故障樹的功能，生成對應(yīng)的故障樹.故障樹顯示如何達(dá)到與TLE相對應(yīng)的狀態(tài)，即通過AND和OR門連接可能導(dǎo)致TLE的基本事件序列(故障).

通過運(yùn)行故障樹，頂層事件“bscu fail twice”得到兩個文件：wbs_000001.flt_events和wbs_000001.flt_gates.其中wbs_000001.flt_events包含三個基本事件，分別是：

1)E2：bscu.lru1.mon._errorSubcomponent.#invalidReport

它表示BSCU子系統(tǒng)的lru1子系統(tǒng)的監(jiān)控單元發(fā)生了invalidReport故障.

2)E5：power._errorSubcomponent.#close

它表示電源組件發(fā)生了close故障.

3)E6：power._errorSubcomponent.#depleted

它表示電源組件發(fā)生了deplted故障.

圖6 “bscu fail twice”的故障樹Fig.6 Fault tree of “bscu fail twice”

圖6是導(dǎo)致頂層事件“bscu fail twice”發(fā)生的故障樹.如圖所示，在這個故障樹中有兩個分支引起故障：一個分支是E2和E5，它們通過與門連接，一起導(dǎo)致事件fault_cfg_1的發(fā)生；另一個分支是E2和E6，也通過與門連接，導(dǎo)致事件fault_cfg_2的發(fā)生.該故障樹的邏輯公式表示為：(E2∧E5)∨(E2∧E6).

故障樹的最小割集(Minimum cutset，MCS)[25]是導(dǎo)致TLE發(fā)生的組件故障的最小組合，它代表對TLE的更簡單的解釋.TLE是MCS的析取，每個割集則是相應(yīng)基本故障事件的合取.“bscu fail twice”的MCS共兩個，為E2∧E5和E2∧E6.

4.3.2 故障模式和影響分析

FMEA以表格的形式顯示了可能導(dǎo)致一個或多個故障狀態(tài)的所有可能的事件組合.本次生成FMEA表依據(jù)的屬性為：“bscu.mode=mode：Backup”.此屬性表示的含義是：BSCU主模式失效.結(jié)果表明為了引發(fā)事件“bscu.mode=mode：Backup”，故障事件組合有以下幾種情況.

1)基數(shù)為1的1個組合：

即“bscu.lru1.mon._errorSubcomponent.# invalidReport=True”.它代表BSCU子系統(tǒng)中的lru1的監(jiān)控單元發(fā)生故障invalidReport.

2)基數(shù)為2的4種組合：

即“(hydr.green_pump._errorSubcomponent.# hydraulicError=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True)”.它代表液壓調(diào)節(jié)系統(tǒng)的綠色液壓泵出現(xiàn)故障hydraulicError并且BSCU子系統(tǒng)中的lru1的監(jiān)控單元發(fā)生故障invalidReport.

以及“(hydr.green_pump._errorSubcomponent.# stuck_at_zero=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True)”.它代表液壓調(diào)節(jié)系統(tǒng)的綠色液壓泵出現(xiàn)故障stuck_at_zero并且BSCU子系統(tǒng)中的lru1的監(jiān)控單元發(fā)生故障invalidReport.

以及“(power._errorSubcomponent.# close=True &bscu.lru1.mon._errorSubcomponent.#invalidReport=True)”.它代表電源組件出現(xiàn)故障close，并且BSCU子系統(tǒng)中的lru1的監(jiān)控單元發(fā)生故障invalidReport.

以及“(power._errorSubcomponent.# depleted=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True)”.它代表電源組件出現(xiàn)depleted的故障，并且BSCU子系統(tǒng)中的lru1的監(jiān)控單元發(fā)生故障invalidReport.

3)基數(shù)為3的4種組合：

即“(power._errorSubcomponent.# close=True &(bscu.lru1.mon._errorSubcomponent.#invalidReport=True &hydr.green_pump._errorSubcomponent.#hydraulicError=True))”.它代表電源組件出現(xiàn)故障close，BSCU子系統(tǒng)中的lru1的監(jiān)控單元發(fā)生故障invalidReport，以及液壓調(diào)節(jié)系統(tǒng)的綠色液壓泵出現(xiàn)故障hydraulicError.

以及“(power._errorSubcomponent.#depleted=True &(bscu.lru1.mon._errorSubcomponent.#invalidReport=True &hydr.green_pump._errorSubcomponent.# hydraulicError=True))”.它代表電源組件出現(xiàn)故障depleted，BSCU子系統(tǒng)中的lru1的監(jiān)控單元發(fā)生故障invalidReport，并且液壓調(diào)節(jié)系統(tǒng)的綠色液壓泵出現(xiàn)故障hydraulicError.

以及“(power._errorSubcomponent.#depleted=True &(hydr.green_pump._errorSubcomponent.# stuck_at_zero=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True))”.它代表電源組件出現(xiàn)故障depleted，液壓調(diào)節(jié)系統(tǒng)的綠色液壓泵出現(xiàn)故障stuck_at_zero并且BSCU子系統(tǒng)中的lru1的監(jiān)控單元發(fā)生故障invalidReport.

以及“(power._errorSubcomponent.#close=True &(hydr.green_pump._errorSubcomponent.#stuck_at_zero=True &bscu.lru1.mon._errorSubcomponent.#invalidReport=True))”.它代表電源組件出現(xiàn)故障close，BSCU子系統(tǒng)中的lru1的監(jiān)控單元發(fā)生故障invalidReport并且液壓調(diào)節(jié)系統(tǒng)的綠色液壓泵出現(xiàn)故障stuck_at_zero.

5 相關(guān)工作與小結(jié)

為了提高安全關(guān)鍵性系統(tǒng)的安全性，使用基于模型的安全評估技術(shù)對復(fù)雜系統(tǒng)進(jìn)行形式化建模和安全性分析受到了學(xué)術(shù)界和工業(yè)界的關(guān)注.文獻(xiàn)[7]提供了AADL的語法，介紹了它的接口和具體實現(xiàn)，并通過示例的講解為AADL對大型系統(tǒng)的建模提供了思路.文獻(xiàn)[9]詳細(xì)介紹了AIR6110標(biāo)準(zhǔn)中的機(jī)輪剎車系統(tǒng)(WBS)，描述了它的架構(gòu)以及功能需求，本文選擇了它的最新架構(gòu)圖進(jìn)行建模和分析.

與已有工作相比，本研究主要工作為：將WBS分為整體層、子系統(tǒng)層及設(shè)備層，采用AADL的子集SLIM對其進(jìn)行系統(tǒng)級建模，充分考慮了組件之間的交互；針對文獻(xiàn)[9]未說明BSCU的命令如何傳到關(guān)閉閥從而對關(guān)閉閥進(jìn)行控制，形式化建模時，在BSCU系統(tǒng)中單獨建了一個select系統(tǒng)，它接受來自于監(jiān)控單元的數(shù)據(jù)，用于判斷是否使用備用液壓，它的輸出select_alternate會傳到關(guān)閉閥從而對關(guān)閉閥進(jìn)行控制；考慮WBS可能發(fā)生的故障并設(shè)計一系列故障模式，選擇指定故障與系統(tǒng)正常功能行為合并為擴(kuò)展模型，從而進(jìn)行安全性分析.

盡管本文的研究結(jié)果論證了基于模型的安全分析方法對于提高安全關(guān)鍵性系統(tǒng)的安全性是有效的，但仍存在不足之處.未來的工作主要分為以下三部分：

1)本文建立的WBS的SLIM模型尚有改進(jìn)空間，在建模時對于液壓調(diào)節(jié)系統(tǒng)的所有子組件，只考慮了液壓的輸入和輸出，而沒考慮子組件造成液壓的損耗.因此，下一步將完善機(jī)輪剎車系統(tǒng)的形式化模型；

2)對于模型的安全性分析，目前只考慮了定性屬性，接下來會在模型中增加概率性屬性[26]，進(jìn)一步對WBS進(jìn)行性能分析；

3)本文研究是從系統(tǒng)的架構(gòu)層出發(fā)，未來將考慮系統(tǒng)的需求層面，證明WBS需求的一致性和完備性.