基于模型檢驗的飛機系統(tǒng)安全性分析方法研究

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

（南京航空航天大學民航學院，南京 210016）

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

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

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

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

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

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

1.1 模型檢驗方法簡介

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

圖1 模型檢驗方法示意圖Fig.1 Sketch of model checking

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

1.2 基于模型檢驗的安全性分析方法

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

1.2.1 準備工作

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

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

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

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

1.2.2 系統(tǒng)建模

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

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

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

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

1.2.3 安全評估

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

2 實例應用

SAE ARP4761附錄中機輪剎車系統(tǒng)（wheel brake system）因為本身的規(guī)模大小和復雜程度適于分析演示，并且在民用安全分析領域的認知度高，所以本文以其為例，使用模型檢驗的方法，對其安全性進行了分析。

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

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

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

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

利用NuSMV語言寫出描述機輪剎車頂層系統(tǒng)功能的代碼。以液壓源為例，液壓源在飛機液壓系統(tǒng)中的動力來源于飛機發(fā)動機或電動泵。然而在機輪剎車系統(tǒng)中，將液壓源簡化為一個無輸入，輸出為液壓能力的元件，其NuSMV代碼如圖4所示。state為液壓狀態(tài)，一般包括正常工作模式和失效模式，因為后面分析中插入的是基本失效狀態(tài)，所以在此選擇布爾型。pressure為輸出壓力狀態(tài)，在定性的分析中簡化為布爾型已經(jīng)可以滿足分析需要，在定量的分析中，則詳細數(shù)值來支持模型建立。

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

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

2.2 安全性分析

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

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

表2 事件定義Tab.2 Event definition

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

3 結語

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

[1]CCAR-25-R3，運輸類飛機適航標準[S].中國民用航空總局，2005.

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

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

[4]CCAR-27-R1，正常類旋翼航空器適航規(guī)定[S].中國民用航空總局，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]燕 飛.軌道交通列車運行控制系統(tǒng)的形式化建模和模型檢驗方法研究[D].北京：北京交通大學，2006.

[12]袁志斌.基于模擬理論的模型檢測研究[D].武漢：華中科技大學，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/.