吳海橋，劉 超，葛紅娟，王華偉

（南京航空航天大學(xué)民航學(xué)院，南京 210016）

機(jī)載系統(tǒng)是現(xiàn)代飛機(jī)的重要組成部分，重要的適航標(biāo)準(zhǔn)均在第1309條對(duì)機(jī)載系統(tǒng)的安全性提出了明確要求，并指出必須通過分析來表明對(duì)該條款的符合性[1-4]。

研究發(fā)現(xiàn)，故障樹分析（fault tree analysis，F(xiàn)TA）等傳統(tǒng)安全性分析方法，主要依靠分析人員的技能和經(jīng)驗(yàn)，受人類認(rèn)知能力的限制，難以預(yù)測(cè)系統(tǒng)所有可能的行為（包括正常和異常行為），容易疏漏某些系統(tǒng)失效狀態(tài)或者誤判系統(tǒng)失效的影響，不適用于當(dāng)前高度復(fù)雜與綜合的機(jī)載系統(tǒng)，經(jīng)過評(píng)估的個(gè)別系統(tǒng)仍發(fā)生了未曾預(yù)料的失效[5]。為此，2001年開始將計(jì)算機(jī)學(xué)科形式化驗(yàn)證中的模型檢驗(yàn)（model checking）引入復(fù)雜機(jī)載系統(tǒng)的安全性評(píng)估領(lǐng)域[6]。

基于模型檢驗(yàn)的飛機(jī)系統(tǒng)安全性分析方法，利用遍歷算法，既可以從數(shù)學(xué)上保證搜索出系統(tǒng)的所有狀態(tài)，不會(huì)發(fā)生疏漏；又可以利用計(jì)算機(jī)工具運(yùn)行算法，自動(dòng)實(shí)現(xiàn)FTA分析目的，減少對(duì)分析人員技能和經(jīng)驗(yàn)的依賴。

目前，基于模型檢驗(yàn)的方法已成為復(fù)雜機(jī)載系統(tǒng)安全性分析的發(fā)展趨勢(shì)之一。歐盟在過去10余年間先后完成了ESACS（enhanced safety assessment for complex systems）[6]和 ISAAC（improvement of safety activities on aeronautical complex systems）[7]兩個(gè)項(xiàng)目，目前正在進(jìn)行MISSA（more integrated systems safety assessment）[8-9]項(xiàng)目，美國(guó)航空航天局（NASA）也開展了類似研究[10]，國(guó)內(nèi)尚無該領(lǐng)域的研究報(bào)道。

本文利用模型檢驗(yàn)方法自動(dòng)實(shí)現(xiàn)FTA的分析目的，即識(shí)別導(dǎo)致頂事件發(fā)生的最小失效組合（即最小割集），提出一種基于模型檢驗(yàn)的飛機(jī)系統(tǒng)安全性分析方法。

1 基于模型檢驗(yàn)的飛機(jī)系統(tǒng)安全性分析方法

1.1 模型檢驗(yàn)方法簡(jiǎn)介

模型檢驗(yàn)方法最早由 Clarke、Emerson以及Quielle、Sifakis于1981年分別提出，可從數(shù)學(xué)上完備地證明或驗(yàn)證所實(shí)現(xiàn)的系統(tǒng)是否與規(guī)范（Specification）一致。模型檢驗(yàn)首先將系統(tǒng)模型轉(zhuǎn)化為一個(gè)有限狀態(tài)機(jī)，如Kripke結(jié)構(gòu)。再將描述系統(tǒng)特性的系統(tǒng)規(guī)范表示為一組時(shí)態(tài)邏輯公式，如計(jì)算樹邏輯（CTL）。最后使用檢驗(yàn)工具驗(yàn)證狀態(tài)轉(zhuǎn)移關(guān)系是否滿足邏輯公式，如果不滿足，驗(yàn)證工具將會(huì)給出一個(gè)反例，其示意圖如圖1所示[11]。

圖1 模型檢驗(yàn)方法示意圖Fig.1 Sketch of model checking

最初發(fā)展起來的模型檢驗(yàn)工具以顯式表示系統(tǒng)狀態(tài)及其轉(zhuǎn)移結(jié)構(gòu)，容易出現(xiàn)狀態(tài)爆炸的問題。而符號(hào)模型檢驗(yàn)（symbolic model checking，SMC）方法的引入，大大地緩解了狀態(tài)空間爆炸問題，基于該方法開發(fā)的模型檢驗(yàn)工具已用于狀態(tài)數(shù)目超過10120的硬件電路的驗(yàn)證[12]。

1.2 基于模型檢驗(yàn)的安全性分析方法

本文提出的基于模型檢驗(yàn)的飛機(jī)系統(tǒng)安全性分析方法，旨在識(shí)別導(dǎo)致頂事件發(fā)生的最小失效組合（即最小割集），實(shí)現(xiàn)FTA的分析目的。該方法的流程如圖2所示。

1.2.1 準(zhǔn)備工作

建模準(zhǔn)備工作的主要目的是獲取模型檢驗(yàn)所需的飛機(jī)系統(tǒng)相關(guān)信息。對(duì)飛機(jī)系統(tǒng)安全性分析前，需要做的準(zhǔn)備工作包括：確定用戶要求，獲取現(xiàn)行的適航認(rèn)證文件，明確系統(tǒng)功能，了解用戶對(duì)安全分析的期望和要求等。通過對(duì)獲取的系統(tǒng)資料分析，確定系統(tǒng)需求規(guī)范（system requirement specification），系統(tǒng)需求規(guī)范通常包括系統(tǒng)及其分系統(tǒng)的定義、構(gòu)成、性能參數(shù)等內(nèi)容。

圖2 基于模型檢驗(yàn)的安全性分析方法的流程Fig.2 Safety analysis process based on model checking

系統(tǒng)模型化是在熟悉系統(tǒng)需求規(guī)范的基礎(chǔ)上，對(duì)飛機(jī)系統(tǒng)的功能、層次、結(jié)構(gòu)以及系統(tǒng)輸入輸出內(nèi)容的抽象過程。系統(tǒng)需求規(guī)范雖然包括建模所需要的所有信息，但是模型建立時(shí)要考慮模型層次和模型復(fù)雜度的問題，尤其對(duì)于復(fù)雜的飛機(jī)系統(tǒng)，單層模型往往不能夠描述整個(gè)系統(tǒng)功能。因此多層子系統(tǒng)之間接口和架構(gòu)、同層系統(tǒng)內(nèi)部模塊接口和功能、模塊的復(fù)雜度等問題都是系統(tǒng)模型化要解決的問題。系統(tǒng)模型化的結(jié)果是以偽代碼描述的飛機(jī)系統(tǒng)初始模型。

通過系統(tǒng)需求定義可獲得飛機(jī)系統(tǒng)的外部功能描述，即系統(tǒng)規(guī)范。失效模式定義確定系統(tǒng)或其部件發(fā)生功能喪失或者故障的方式。系統(tǒng)安全性需求確定系統(tǒng)部件功能失效或故障對(duì)系統(tǒng)狀態(tài)的影響。

1.2.2 系統(tǒng)建模

系統(tǒng)建模主要包括形式化建模和系統(tǒng)模型擴(kuò)展：1）形式化建模

形式化建模是將飛機(jī)系統(tǒng)初始模型和系統(tǒng)規(guī)范轉(zhuǎn)化為模型檢驗(yàn)工具驗(yàn)證代碼的過程。因?yàn)轱w機(jī)系統(tǒng)正常模型的功能要符合系統(tǒng)規(guī)范，同時(shí)模型的描述語(yǔ)言要遵循模型檢驗(yàn)工具的語(yǔ)言規(guī)范，所以模型建立后，首先要驗(yàn)證其是否滿足系統(tǒng)規(guī)范。這一點(diǎn)可以通過模型檢驗(yàn)工具實(shí)現(xiàn)。如果模型通過驗(yàn)證，則飛機(jī)系統(tǒng)正常模型建立完成；如果系統(tǒng)模型沒有通過驗(yàn)證，可能是飛機(jī)系統(tǒng)設(shè)計(jì)存在缺陷或者模型建立存在錯(cuò)誤。如果是系統(tǒng)設(shè)計(jì)存在缺陷，則要修改系統(tǒng)設(shè)計(jì)，再對(duì)系統(tǒng)重新進(jìn)行建模驗(yàn)證；如果是系統(tǒng)模型存在問題或者系統(tǒng)規(guī)范的時(shí)序邏輯描述錯(cuò)誤，則要修改系統(tǒng)模型或者時(shí)序邏輯描述。

2）系統(tǒng)模型擴(kuò)展

系統(tǒng)模型擴(kuò)展是向飛機(jī)系統(tǒng)正常模型中的部件狀態(tài)添加失效模式的過程，在基于模型檢驗(yàn)的飛機(jī)系統(tǒng)安全性分析過程中，除了考慮元件（系統(tǒng)）正常的工作模式（狀態(tài)）外還要考慮其失效模式（狀態(tài)）。這是模型檢驗(yàn)方法在應(yīng)用于飛機(jī)系統(tǒng)時(shí)的特別之處。

1.2.3 安全評(píng)估

利用模型檢驗(yàn)工具實(shí)現(xiàn)的算法，可以對(duì)飛機(jī)系統(tǒng)狀態(tài)進(jìn)行搜索。假設(shè)飛機(jī)系統(tǒng)功能在系統(tǒng)需求定義被描述為系統(tǒng)規(guī)范表達(dá)式p，那么時(shí)序邏輯表達(dá)式“AG p”為真，表示飛機(jī)系統(tǒng)在任何條件下都具有這個(gè)功能；邏輯表達(dá)式“EF p”為真，表示飛機(jī)系統(tǒng)中具有這個(gè)功能但僅在特定的條件下有效。通過對(duì)得到飛機(jī)系統(tǒng)失效模型狀態(tài)分析，也能夠得到相應(yīng)安全性分析結(jié)果，如本文下面舉例的與最小割集等價(jià)的最小失效組合。

2 實(shí)例應(yīng)用

SAE ARP4761附錄中機(jī)輪剎車系統(tǒng)（wheel brake system）因?yàn)楸旧淼囊?guī)模大小和復(fù)雜程度適于分析演示，并且在民用安全分析領(lǐng)域的認(rèn)知度高，所以本文以其為例，使用模型檢驗(yàn)的方法，對(duì)其安全性進(jìn)行了分析。

2.1 剎車系統(tǒng)建模

機(jī)輪剎車系統(tǒng)是飛機(jī)起落架系統(tǒng)的子系統(tǒng)，在飛機(jī)滑行、著陸和中斷起飛的情況下，起到對(duì)飛機(jī)機(jī)輪安全減速的作用[13]。

以機(jī)輪剎車系統(tǒng)的頂層系統(tǒng)為分析對(duì)象，為了簡(jiǎn)便說明，不考慮原有系統(tǒng)中的防滑功能。系統(tǒng)輸入為人工剎車時(shí)的腳蹬位置或自動(dòng)剎車時(shí)用戶面板設(shè)定的剎車速率，系統(tǒng)輸出為機(jī)輪接收到的液壓壓力。建立剎車系統(tǒng)模型，且對(duì)模塊進(jìn)行編號(hào)以簡(jiǎn)化后續(xù)輸出，如圖3所示。

選用NuSMV作為模型檢驗(yàn)工具。NuSMV源于CMU開發(fā)的基于BDD的模型檢驗(yàn)器CMU SMV，它是一個(gè)高水平的符號(hào)模型檢驗(yàn)器。NuSMV允許同步和異步有限狀態(tài)的表示，它使用基于BDD和基于SAT的檢驗(yàn)技術(shù)進(jìn)行模型檢驗(yàn)，并且支持對(duì)強(qiáng)公正約束的檢驗(yàn)支持[14]。

利用NuSMV語(yǔ)言寫出描述機(jī)輪剎車頂層系統(tǒng)功能的代碼。以液壓源為例，液壓源在飛機(jī)液壓系統(tǒng)中的動(dòng)力來源于飛機(jī)發(fā)動(dòng)機(jī)或電動(dòng)泵。然而在機(jī)輪剎車系統(tǒng)中，將液壓源簡(jiǎn)化為一個(gè)無輸入，輸出為液壓能力的元件，其NuSMV代碼如圖4所示。state為液壓狀態(tài)，一般包括正常工作模式和失效模式，因?yàn)楹竺娣治鲋胁迦氲氖腔臼顟B(tài)，所以在此選擇布爾型。pressure為輸出壓力狀態(tài)，在定性的分析中簡(jiǎn)化為布爾型已經(jīng)可以滿足分析需要，在定量的分析中，則詳細(xì)數(shù)值來支持模型建立。

系統(tǒng)功能規(guī)范描述為機(jī)輪能接收到剎車壓力，用計(jì)算樹邏輯語(yǔ)言可以描述為“AG!Wheel.pressurefail”。利用NuSMV對(duì)包含有系統(tǒng)模型和時(shí)序邏輯的代碼文件進(jìn)行檢驗(yàn)，輸出結(jié)果為“AG!Wheel.pressurefail is TRUE”，說明模型功能滿足系統(tǒng)需求，至此系統(tǒng)正常模型建立完成。

在系統(tǒng)正常的模塊中插入失效狀態(tài)，建立擴(kuò)展系統(tǒng)模型。本例中對(duì)除機(jī)輪以外的模塊，插入標(biāo)準(zhǔn)失效狀態(tài)。標(biāo)準(zhǔn)失效狀態(tài)下的模塊，狀態(tài)有TRUE和FALSE兩種情況，在TRUE狀態(tài)下，模塊可用且下一狀態(tài)是TRUE或FALSE。在FALSE狀態(tài)下，模塊失效且下一狀態(tài)始終為FALSE。

2.2 安全性分析

完成擴(kuò)展系統(tǒng)模型的建立后，本文利用NuSMV自動(dòng)驗(yàn)證了模塊和模塊組合的失效對(duì)系統(tǒng)功能的影響。使用 CTL 公式“EG（p→ q）”，其中 q為”Wheel.pressurefail”，p為模塊和模塊組合失效狀態(tài)，總共有1 024（210）種情況，通過枚舉驗(yàn)證一共有13種最小失效組合（即最小割集），如表1所示，其中事件定義如表2所示。

表1 最小失效組合Tab.1 Minimum failure combination

表2 事件定義Tab.2 Event definition

為檢驗(yàn)本文方法的正確性，對(duì)上述系統(tǒng)使用FTA建立故障樹，如圖5所示。將表1中的最小失效組合與通過傳統(tǒng)FTA得到最小割集進(jìn)行了對(duì)比，兩者完全相同，表明本文方法可以自動(dòng)實(shí)現(xiàn)FTA的分析目的。

3 結(jié)語(yǔ)

基于模型檢驗(yàn)的飛機(jī)系統(tǒng)安全性分析方法，利用模型檢驗(yàn)方法，列出模型系統(tǒng)的狀態(tài)，并用特定算法按照邏輯表達(dá)式描述對(duì)系統(tǒng)狀態(tài)進(jìn)行搜索檢驗(yàn)，自動(dòng)得出與FTA最小割集等價(jià)的最小失效組合。本文方法既可從數(shù)學(xué)上保證搜索系統(tǒng)所有的狀態(tài)，不會(huì)發(fā)生疏漏；又可利用模型檢驗(yàn)工具軟件，自動(dòng)實(shí)現(xiàn)FTA分析目的，減少對(duì)分析人員技能和經(jīng)驗(yàn)的依賴。隨著模型檢驗(yàn)方法的不斷發(fā)展，其能夠處理的狀態(tài)數(shù)量可基本滿足復(fù)雜機(jī)載系統(tǒng)安全性分析的需要，基于模型檢驗(yàn)的方法業(yè)已成為復(fù)雜機(jī)載系統(tǒng)安全性分析技術(shù)的發(fā)展趨勢(shì)之一。

[1]CCAR-25-R3，運(yùn)輸類飛機(jī)適航標(biāo)準(zhǔn)[S].中國(guó)民用航空總局，2005.

[2]CCAR-23-R3，正常類、實(shí)用類、特技類和通勤類飛機(jī)適航規(guī)定[S].中國(guó)民用航空總局，2005.

[3]CCAR-29-R1，運(yùn)輸類旋翼航空器適航規(guī)定[S].中國(guó)民用航空總局，2002.

[4]CCAR-27-R1，正常類旋翼航空器適航規(guī)定[S].中國(guó)民用航空總局，2002.

[5]JOHN RUSHBY.Formalism in Safety Cases[C]//Making Systems Safer.London：Springer-Verlag London Limited，2010：3-17.

[6]?KERLUND O，BIEBER P，B?DE E，et al.ESACS：an Integrated Methodology for Design and Safety Analysis of Complex Systems[C]//European Safety and Reliability Conference（ESREL）.Toulouse：Balkema publisher，2003：203-221.

[7]?KERLUND O，BIEBER P，B?DE E，et al.ISAAC，a Framework for Integrated Safety Analysis of Functional，Geometrical and Human As pects[C]//ElectronicReciprocalTransferSystem，Toulouse.France：2006：145-162.

[8]VALéRIE SARTOR，JEAN GAUTHIER.Model Based Safety Assessment In Dassault Aviation[C]//Model-based Safety Assessment（Journées MISSA）：2010，12：11-15.

[9]LAURENT SAGASPE NICOLAS MAY.MBSA in Aeronautics Experience Feed-back on modelling applications[C]//Model Based Safety AssessmentWorkshop（MBSAW2011），Toulouse.France：2011：53-59.

[10]ANJALI JOSHI，MICHAEL W WHALEN，MATS P E HEIMDAHL.Model-Based Safety Analysis Final Report[R].NASA/CR-2006-213953，NASA Contractor Report，2006.

[11]燕 飛.軌道交通列車運(yùn)行控制系統(tǒng)的形式化建模和模型檢驗(yàn)方法研究[D].北京：北京交通大學(xué)，2006.

[12]袁志斌.基于模擬理論的模型檢測(cè)研究[D].武漢：華中科技大學(xué)，2007.

[13]SAE.Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment[R].SAE ARP4761，1996.

[14]ROBERTO CAVADA，ALESSANDRO CIMATTI，CHARLES ARTHUR JOCHIM，et al.NuSMV 2.5 User Manual[EB/OL].[2011-12-01]http：//nusmv.fbk.eu/.