一個(gè)基于形式化方法的系統(tǒng)安全性建模分析實(shí)例研究

石夢(mèng)燁，胡 軍，陳 朔，唐紅英，王立松

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

1 引 言

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

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

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

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

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

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

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

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

2.1 MBSA框架

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

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

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

2.2 MBSA中的形式化方法

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

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

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

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

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

在本文的工作中，選擇了在SAE的AIR6110標(biāo)準(zhǔn)中所給出的一個(gè)典型的安全關(guān)鍵系統(tǒng)實(shí)例展開研究，這是一個(gè)航空領(lǐng)域中的飛機(jī)機(jī)輪剎車系統(tǒng)的系統(tǒng)規(guī)范和安全性分析實(shí)例.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è)備安全評(píng)估程序的指南和方法”[20]中的要求.ARP4754和ARP4761是目前航空電子領(lǐng)域的開發(fā)和安全評(píng)估過程的工業(yè)標(biāo)準(zhǔn).

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

在AIR6110所給出的這個(gè)實(shí)例系統(tǒng)中，主要描述了WBS的系統(tǒng)框架結(jié)構(gòu)和功能要求，其中，WBS由制動(dòng)系統(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)行計(jì)算并向液壓調(diào)節(jié)系統(tǒng)輸出不同命令：傳輸?shù)揭簤赫{(diào)節(jié)系統(tǒng)正常線路的控制命令，傳輸?shù)揭簤赫{(diào)節(jié)系統(tǒng)備用線路的控制命令，對(duì)關(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ā)出錯(cuò)誤警報(bào)，則由選擇設(shè)備自動(dòng)切換成備用組.

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

3.2 WBS的形式化建模

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

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

模型層級(jí)系統(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所示，其他部件可以通過類似方法得到其對(duì)應(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個(gè)轉(zhuǎn)換說明，如果收到的數(shù)據(jù)端口綠色液壓值大于等于5，則說明使用正常線路，那么令液壓值等于輸入的綠色液壓值.

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

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

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

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

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

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

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

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

3.3.1 故障設(shè)置

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

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

1)OK-[Internal_error]->Dead；

2)OK-[stuck_at_zero]->Stuck_at_zero.

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

3.3.2 故障擴(kuò)展

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

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

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

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

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

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

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

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

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

4.2 模型檢測(cè)

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

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

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

接下來對(duì)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)是失效，可能會(huì)響應(yīng)警報(bào)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，即兩個(gè)監(jiān)控命令單元都失效.這種情況下，說明整個(gè)BSCU子系統(tǒng)已經(jīng)失效.使用COMPASS中生成故障樹的功能，生成對(duì)應(yīng)的故障樹.故障樹顯示如何達(dá)到與TLE相對(duì)應(yīng)的狀態(tài)，即通過AND和OR門連接可能導(dǎo)致TLE的基本事件序列(故障).

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

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ā)生的故障樹.如圖所示，在這個(gè)故障樹中有兩個(gè)分支引起故障：一個(gè)分支是E2和E5，它們通過與門連接，一起導(dǎo)致事件fault_cfg_1的發(fā)生；另一個(gè)分支是E2和E6，也通過與門連接，導(dǎo)致事件fault_cfg_2的發(fā)生.該故障樹的邏輯公式表示為：(E2∧E5)∨(E2∧E6).

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

4.3.2 故障模式和影響分析

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

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

即“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)的安全性，使用基于模型的安全評(píng)估技術(shù)對(duì)復(fù)雜系統(tǒng)進(jìn)行形式化建模和安全性分析受到了學(xué)術(shù)界和工業(yè)界的關(guān)注.文獻(xiàn)[7]提供了AADL的語(yǔ)法，介紹了它的接口和具體實(shí)現(xiàn)，并通過示例的講解為AADL對(duì)大型系統(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對(duì)其進(jìn)行系統(tǒng)級(jí)建模，充分考慮了組件之間的交互；針對(duì)文獻(xiàn)[9]未說明BSCU的命令如何傳到關(guān)閉閥從而對(duì)關(guān)閉閥進(jìn)行控制，形式化建模時(shí)，在BSCU系統(tǒng)中單獨(dú)建了一個(gè)select系統(tǒng)，它接受來自于監(jiān)控單元的數(shù)據(jù)，用于判斷是否使用備用液壓，它的輸出select_alternate會(huì)傳到關(guān)閉閥從而對(duì)關(guān)閉閥進(jìn)行控制；考慮WBS可能發(fā)生的故障并設(shè)計(jì)一系列故障模式，選擇指定故障與系統(tǒng)正常功能行為合并為擴(kuò)展模型，從而進(jìn)行安全性分析.

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

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

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

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