張維珺，胡 軍，李宛倩，陳 朔，石夢燁，唐紅英

南京航空航天大學 計算機科學與技術學院，南京 211106

1 引言

20世紀70年代，飛機電子系統(tǒng)迅速向數(shù)字化、綜合化和模塊化方向發(fā)展，80年代末更是出現(xiàn)了綜合模塊化航空電子系統(tǒng)（integrated modular avionics，IMA）[1]的概念。微電子和軟件技術的迅速發(fā)展使得綜合模塊化航空電子系統(tǒng)[2]日益成熟，其包含的系統(tǒng)組件逐漸完善。然而，隨著系統(tǒng)中各組件之間的交互變得更加緊密，組件之間的相互作用更可能產(chǎn)生故障進而演變成事故，機載系統(tǒng)的安全性至關重要。

近年來，基于模型的安全性分析技術及其應用越來越受到工業(yè)界的關注，在航空等領域有著廣泛應用。相關學者亦對其進行研究和實踐，例如使用MBSA（model-based safety analysis method）[3]方法及NuSMV（new symbolic model verifier）語言對飛控系統(tǒng)的前主槳舵機進行建模與驗證[4]；基于MBSA對高速鐵路牽引供電系統(tǒng)進行安全風險評估[5]；分析及驗證MBSA能夠解決傳統(tǒng)安全性分析中飛機級安全性評估不足的問題[6]等。

本文主要研究以xSAP（extended safety assessment platform）系統(tǒng)安全性評估平臺為核心的MBSA方法，對實際數(shù)字自動飛行控制系統(tǒng)GFC700中的飛行引導系統(tǒng)進行需求性建模、系統(tǒng)故障設計以及安全性分析。

文章組織結(jié)構(gòu)安排如下：第2章簡單介紹基于模型的系統(tǒng)安全性評估技術和形式化模型；第3章介紹基于形式化模型的系統(tǒng)安全性分析框架及其核心問題，即層次化建模、故障注入以及模型擴展等；第4章簡要介紹飛行引導系統(tǒng)，詳細闡述對其設計的兩種故障模式，描述如何使用xSAP平臺對飛行引導系統(tǒng)進行形式化建模、故障設計以及模型擴展，運行xSAP工具對飛行引導系統(tǒng)進行安全性分析，生成故障樹[7]及 FMEA（failure mode and effect analysis）表[8]；第 5章對已有工作進行總結(jié)。

2MBSA和形式化模型

2.1 基于模型的安全性分析方法

基于模型的安全性分析方法（MBSA）采用一種基于模型的系統(tǒng)開發(fā)過程去創(chuàng)建一個“共享的系統(tǒng)模型”,這個共享的系統(tǒng)模型可以同時被系統(tǒng)設計過程和系統(tǒng)安全評估過程所使用[9]，即在系統(tǒng)設計過程中使用一種建模語言描述正常運行條件下的系統(tǒng)架構(gòu)以及安全關鍵功能行為，在系統(tǒng)安全評估過程中基于所建立的系統(tǒng)正常模型進行失效行為的語義擴展，生成用于安全性分析的故障擴展模型。

2.2 形式化建模與分析

形式化方法即在對計算機系統(tǒng)中的硬件和軟件進行規(guī)約、設計和分析的過程中所使用的基于數(shù)學理論的描述形式和分析技術。在系統(tǒng)工程領域中，對于系統(tǒng)建模而言，采用基于數(shù)學語義的形式化建模語言可以使得所建立的系統(tǒng)模型具有嚴格的語法和語義定義，采用形式化分析的技術可以對系統(tǒng)模型進行分析和判定，進而支持和指導系統(tǒng)的開發(fā)過程。因此形式化方法在基于模型的系統(tǒng)工程中極為重要。

3 基于形式化模型的系統(tǒng)安全性分析

3.1 基于形式化模型的系統(tǒng)安全性分析框架

圖1給出了基于形式化模型的系統(tǒng)安全性分析框架。起點是基于系統(tǒng)需求的形式化模型，通常它只包含正常系統(tǒng)的功能行為，即沒有考慮故障行為。該模型或直接被使用于系統(tǒng)的安全性與功能性驗證，或被進行故障注入與模型擴展，而后用于系統(tǒng)的故障分析等安全性評估。需要注意的是將正常模型擴展成系統(tǒng)故障模型的過程基于故障注入的概念，即不能一次性地建立既包含系統(tǒng)正常行為又包含故障行為的模型，否則考慮因素太多，建模過程太復雜。

Fig.1 Framework of system safety analysis based on formal model圖1 基于形式化模型的系統(tǒng)安全性分析框架

基于形式化模型的安全性分析方法的重點是如何構(gòu)建系統(tǒng)的形式化模型以及如何對系統(tǒng)行為中的故障進行設計并將故障擴展到系統(tǒng)正常模型中。層次化建模、故障注入和故障模式及模型擴展是該方法必須解決的核心問題。

3.2 安全框架中的核心問題

3.2.1 層次化建模

一個安全關鍵復雜系統(tǒng)的需求規(guī)約數(shù)量較為龐大，有時甚至有數(shù)千條。如果將這些規(guī)約放在同一層次進行建模和分析，會使得建模工作變得繁雜混亂，對于模型的形式化驗證也可能會出現(xiàn)狀態(tài)空間爆炸的問題，從而無法進行驗證。因此，需要考慮層次化的建模方式，使用漸增式的方法進行分層驗證。以飛行引導系統(tǒng)（flight guidance system，F(xiàn)GS）為例說明分層驗證的必要性。

由于飛行引導系統(tǒng)中的飛行模式總類較多，相互之間存在層次關系，對飛行引導系統(tǒng)完全建模的工作較為復雜，代碼量較大，在運行的過程中錯誤不容易修改，因此將飛行引導系統(tǒng)分為四層，逐層建模，如表1所示。

Table 1 Layer structure of FGS表1 飛行引導系統(tǒng)分層結(jié)構(gòu)

3.2.2 故障注入機制

故障注入機制即在正常功能模型中添加已設定好的故障事件，該事件僅為相應故障模式在正常功能模型中的聲明，亦為將故障模式擴展到正常功能模型的接口。通常一個正常功能模型包含多個功能模塊，故障注入需要應用于每一個模塊。對于同一模塊，需要設置不同的故障模式控制變量；對于不同模塊，可以有相同的故障模式控制變量，以表示不同模塊間的同一種故障事件。故障注入機制如圖2所示。

Fig.2 Fault injection圖2 故障注入機制

3.2.3 故障模式及模型擴展

上述故障注入機制發(fā)生在正常功能模型建模階段，故障模式的設定以及故障模型擴展則發(fā)生在故障分析階段。故障模式的規(guī)約信息被包含在故障事件及相應的控制變量中，而其具體定義則體現(xiàn)在故障擴展指令文件 FEI（fault extension instructions）中。故障模式的具體定義依賴于故障模式模板，由故障分析工具中的故障庫提供。例如，基于模型的安全性分析平臺xSAP會為使用者提供一個故障模式的預定義庫，即通用故障模式庫，其模板包括：反轉(zhuǎn)故障inverted、卡死故障stuck_at(value)（在某個值卡死）及cstuck_at（在某個變量卡死）、隨機random（不確定的輸出）等。在故障模式的設定過程中，可直接使用故障模式庫中已定義好的故障模板，也可自定義故障模板。故障可以被聲明為永久性的或偶發(fā)性的，當故障被聲明為偶發(fā)性時，表明該故障只是暫時出現(xiàn)或者會隨著系統(tǒng)的維修而消失。

模型擴展[10]即為將包含有故障事件的系統(tǒng)正常模型（在模型擴展前，系統(tǒng)模型雖包含有故障事件，但此時故障事件并沒有被明確定義，僅為一個聲明，因此現(xiàn)階段的模型仍為系統(tǒng)正常模型）與已定義的故障模式結(jié)合，形成故障擴展模型，以實現(xiàn)系統(tǒng)安全性評估與分析。

4 飛行引導系統(tǒng)的實例建模與安全性分析

4.1 GFC700實例系統(tǒng)概述

本研究選用了一個某機型上的綜合航電系統(tǒng)（Garmin G1000[11]）中的GFC700自動飛行控制系統(tǒng)來進行實例系統(tǒng)分析驗證。自動飛行控制系統(tǒng)包括飛行引導系統(tǒng)（flight guidance system，F(xiàn)GS）、飛行管理系統(tǒng)（flight management system，F(xiàn)MS）、飛行指引（flight director，F(xiàn)D）、自動駕駛（autopilot，AP）等子系統(tǒng)。其中飛行引導系統(tǒng)主要由模式邏輯以及飛行控制律兩大模塊構(gòu)成。模式邏輯是一組離散算法，其作用是在系統(tǒng)處于激活狀態(tài)的任意時刻，選擇合適的飛行控制律。本文主要研究飛行引導系統(tǒng)的模式邏輯。飛行引導系統(tǒng)的飛行模式[12]通常可分為兩大模塊：橫向模式和垂直模式。橫向模式通過調(diào)整飛機的側(cè)滾角度來控制飛機水平方向的運動。垂直模式通過調(diào)節(jié)飛機的俯仰角度來控制飛機豎直方向的運動。典型的飛行模式見表2。

Table 2 Flight modes表2 飛行模式

由于每一個飛行模式都有三種基本狀態(tài)，即選擇激活狀態(tài)、取消選擇狀態(tài)和默認狀態(tài)，因此針對模式的狀態(tài)設計了兩種模式故障：模式輸出卡死故障和模式輸出紊亂故障。

模式輸出卡死故障即為不論該飛行模式被取消或是選擇，其永遠保持一種狀態(tài)，例如若某一飛行模式卡死在選擇激活狀態(tài)，則無論對其進行取消或選擇操作，該飛行模式永遠保持選擇激活狀態(tài)，如圖3所示；模式輸出紊亂故障即為該飛行模式最終呈現(xiàn)的狀態(tài)與其被指定的狀態(tài)不符，例如若某一飛行模式輸出紊亂，則對其進行選擇操作，該飛行模式可能處于取消選擇狀態(tài)而非選擇激活狀態(tài)，如圖4所示。針對某一飛行模式自身出現(xiàn)的故障，不僅對該飛行模式有影響，也會對與該飛行模式相關聯(lián)的其他飛行模式造成巨大影響。

Fig.3 HDG stuck at selected_state圖3 HDG模式卡死在選擇激活狀態(tài)

Fig.4 Disordered output of HDG圖4 HDG模式輸出紊亂

4.2 基于模型的系統(tǒng)安全性評估平臺xSAP

xSAP[13]是基于模型的系統(tǒng)安全性分析平臺，主要功能包括對系統(tǒng)需求及功能的驗證、模型擴展、系統(tǒng)安全性分析等。該平臺的特點包括：提供可自定義故障模板的故障庫；自動化實現(xiàn)模型擴展；實施全面的安全分析，包括故障樹分析（fault tree analysis，F(xiàn)TA），失效模式與影響分析（FMEA），使用定時故障傳播圖（timed failure propagation graphs，TFPG）的故障傳播分析和共因分析（common cause analysis，CCA）等。

xSAP平臺主要由兩個工具來支持：nuXmv以及xSAP。nuXmv[14]是NuSMV模型檢驗器的擴展版本，主要用于需求分析及需求模型的功能性驗證。NuSMV[15]符號模型檢測器從卡內(nèi)基梅隆大學版本的SMV(symbolic model verifier)模型檢測器演變而來，是基于二元決策圖（binary decision diagrams，BDDS）重新實現(xiàn)的SMV的擴展?；緢?zhí)行思路是將模型狀態(tài)空間用符號化的形式和二元決策圖來存儲和處理。本研究采用的工具版本為NuSMV 2，擴展了NuSMV版本，新增特性包括：結(jié)合基于BDD符號化技術和基于SAT（satisfiability）模型檢測組件的新模型檢測算法及驗證技術等[16]。xSAP主要用于模型擴展和安全性評估。xSAP構(gòu)建在nuXmv上，在SAP中正常模型及故障擴展模型均用nuXmv的形式化語言（NuSMV建模語言）表達，且待驗證安全性屬性也用NuSMV中的時序語言進行構(gòu)造，如全局不變式、線性時序邏輯（linear temporary logic，LTL）或計算樹邏輯（computation tree logic，CTL）公式等[17]。

基于xSAP平臺的系統(tǒng)安全性分析包括對系統(tǒng)進行需求性建模（NuSMV模型），以及根據(jù)系統(tǒng)設計故障模式。通過對NuSMV需求模型進行模型擴展得到故障擴展模型，以實現(xiàn)安全屬性驗證及故障分析。安全性評估與分析主要包含兩方面：第一，使用NuSMV模型驗證工具，以正常NuSMV模型為基礎檢驗系統(tǒng)需求及安全性屬性。其驗證結(jié)果分為兩種：模型符合安全屬性，則該條安全屬性通過驗證，返回True；否則返回False，并給出反例路徑。第二，使用xSAP故障分析工具，以模型擴展后的NuSMV模型為基礎進行故障分析，自動化生成相應的故障樹及FMEA表。圖5即為以xSAP為核心的基于MBSA的系統(tǒng)驗證與安全性分析框架。

Fig.5 Model-based system safety assessment based on xSAP圖5 以xSAP為核心基于模型的系統(tǒng)安全評估

4.3 飛行引導系統(tǒng)建模及模型擴展

4.3.1 NuSMV建模

本研究主要對飛行引導系統(tǒng)的第一層模型進行建模及故障注入。圖6為飛行引導系統(tǒng)初級模型概觀，包括四種常見飛行模式（側(cè)滾模式ROLL、航向選擇模式HDG、俯仰保持模式PITCH和垂直速度模式VS），以及與上述飛行模式相關的飛行儀表和邊緣組件（自動駕駛儀AP和飛行指引儀FD）。

Fig.6 Overview of FGS first level model圖6 飛行引導系統(tǒng)初級層次模型概觀

使用RSML-e（requirements state machine language without events）語言對飛行模式以及邊緣組件進行需求性建模[12]。由于RSML-e模型僅能清晰、詳細、直觀地描述系統(tǒng)需求，并不能被模型檢測工具進行模型驗證，因此將其轉(zhuǎn)換成能夠?qū)崿F(xiàn)安全性屬性驗證的NuSMV模型，此模型即為未包含故障擴展的NuSMV模型。對于模型轉(zhuǎn)換而言，模型間的相似度越高，轉(zhuǎn)換越容易建立[18]。RSML-e模型與NuSMV 2模型相似度較高，具有語義一致性，能夠建立相互間的轉(zhuǎn)換規(guī)則并確保轉(zhuǎn)換規(guī)則的正確性。RSML-e模型到NuSMV 2模型的語法轉(zhuǎn)換包括[19]：類型和變量的轉(zhuǎn)換、轉(zhuǎn)換時的時態(tài)對應關系、狀態(tài)遷移條件轉(zhuǎn)換、扁平化處理以及宏的轉(zhuǎn)換等。

為了驗證該模型的正確性與完整性，以及飛行引導系統(tǒng)需求的安全性與可靠性，設計29條屬性進行模型驗證，內(nèi)容包括圖6中所有飛行模式及邊緣組件的功能性和安全性的驗證。屬性驗證可分為兩部分：第一，對每個組件和模式自身的功能性及安全性進行驗證，例如每個飛行模式是否能夠正常被選擇或者取消；第二，對模式間的交互進行安全性驗證。經(jīng)驗證，該29條屬性均正確，整個驗證耗時0.53 s。驗證結(jié)果的部分截圖如圖7所示。

Fig.7 Verification results of FGS first level model(part)圖7 飛行引導系統(tǒng)初級模型驗證結(jié)果部分截圖

4.3.2 故障注入與不變式的定義

4.3.2.1 故障注入

飛行引導系統(tǒng)初級模型的故障分析重點是對每個模式自身的故障進行分析，因此僅在NuSMV模型中表示模式狀態(tài)變化的狀態(tài)變量中添加故障事件。選擇航向選擇模式（HDG）和垂直速度模式（VS）作為故障擴展單元，對在HDG和VS上可能發(fā)生的故障行為進行擴展。在飛行引導系統(tǒng)初級NuSMV模型的建模過程中，設定HDG和VS狀態(tài)變量的可能取值為Un_Defined、Cleared和Selected。以HDG飛行模式為例具體模型代碼如圖8所示。

Fig.8 NuSMV code of state variable of HDG圖8 航向選擇模式HDG狀態(tài)變量的NuSMV代碼

根據(jù)4.1節(jié)定義的兩種模式故障對HDG和VS模式進行故障注入。

（1）模式輸出卡死故障。結(jié)合NuSMV建模，該故障可能導致模式狀態(tài)變量的取值卡死在Un_Defined或Cleared或Selected，因此該類型故障將有三個故障事件：

--模式的輸出保持Selected，即模式一直處于選擇激活狀態(tài)

fault_event_stuck_at_Selected:boolean;

--模式的輸出保持Cleared，即模式一直處于取消選擇狀態(tài)

fault_event_stuck_at_Cleared:boolean;

--模式的輸出保持Un_Defined，即模式一直處于默認的未被選中狀態(tài)

fault_event_stuck_at_Un_Defined:boolean;

（2）模式輸出紊亂故障。結(jié)合NuSMV建模，當發(fā)生模式輸出紊亂時，模式的輸出值可能為Un_Defined、Cleared及Selected中的任意一個。對該故障模式定義一個故障事件Disorderoutput，即：

--模式的輸出值與正確的輸出值不對應

fault_event_disorderoutput：boolean;

當上述兩類故障事件發(fā)生時，飛行模式不能通過自行修復使得其從失效狀態(tài)變回正常狀態(tài)，因此模式的失效是不可逆的。如下代碼即表示失效狀態(tài)的不可逆：

將上述代碼分別添加到HDG和VS模式中即完成故障注入。

4.3.2.2 不變式

在模型的故障分析中，故障樹及FMEA表均需要頂層失效事件才能得以生成，因此需要在NuSMV模型的驗證屬性中以“INVARSPEC”為關鍵字添加不變式，該不變式的“非”即為相應的頂層失效事件。添加的不變式如下：

INVARSPEC((m_HDG.HDG=Un_Defined)&!(next(m_Select_HDG.result))->next(m_HDG.HDG=Cleared))&(((m_VS.VS=Selected)&next(m_Deselect_VS.result))->next(m_VS.VS=Cleared));

上述不變式由兩條子不變式以“&”關鍵字連接而成，可以驗證兩條屬性的組合故障分析。其中前一條不變式與HDG模式中的狀態(tài)變量HDG相關，后一條不變式與VS模式中的狀態(tài)變量VS相關。該不變式的含義為：在全局狀態(tài)下，如果HDG模式處于默認無操作狀態(tài)且其未被選擇，則HDG模式將處于未被選擇狀態(tài)；同時，如果VS模式處于被選擇狀態(tài)且被取消選擇，則VS模式將處于選擇取消狀態(tài)。經(jīng)驗證，該不變式屬性驗證為真。

4.3.3 FEI故障模式

本小節(jié)將利用xSAP工具中的故障模板，對4.3.2小節(jié)中的兩種故障類型進行詳細定義，編寫FEI文件形式的故障模式。

（1）模式輸出卡死故障。此類卡死故障的故障模板可以在xSAP的故障庫中找到，即“stuckatbyvalue”模板，因此可以根據(jù)該模板定義，直接編寫故障擴展指令文件（FEI）。以HDG模式為例，模式卡死故障包含3個故障事件，其對應的3個故障模式分別為：

stuckAt_Selected：模式的輸出卡死在Selected狀態(tài)。

stuckAt_Cleared：模式的輸出卡死在Cleared狀態(tài)。

stuckAt_Un_Defined：模式的輸出卡死在Un_Defined狀態(tài)。

（2）模式輸出紊亂故障。xSAP故障庫并沒有包含該類故障，因此需要自行定義故障模式模板，根據(jù)自定義模板編寫故障擴展指令文件（FEI）。

①自定義模板：在xSAP工具中自定義故障效果模式disorderoutput，定義該故障效果模式的during事件和entering事件的smv文件，如圖9、圖10所示。

圖9 entering.smv

圖10 during.smv

圖9 中entering.smv文件定義了作用對象從正常狀態(tài)到失效狀態(tài)的效果模式，其中next(varout)!=input表示，當發(fā)生輸出紊亂故障時，得到的輸出結(jié)果與期望的輸出值不一致。

圖10中during.smv文件定義了作用對象一直處于失效狀態(tài)的效果模式，其中next(varout)=varout表示在發(fā)生輸出紊亂故障的過程中，模式輸出值一直處于紊亂狀態(tài)。

輸出紊亂故障模式的狀態(tài)轉(zhuǎn)換圖如圖11所示。

Fig.11 State transition of output disordered fault mode圖11 輸出紊亂故障模式的狀態(tài)轉(zhuǎn)換圖

②故障擴展指令文件：根據(jù)自定義模板編寫FEI文件，以HDG模式為例，模式輸出紊亂故障包含一個故障事件，其對應的故障模式為Disorderoutput_HDG。詳細定義見圖12。

Fig.12 FEI of HDG mode as unit of influence圖12 以HDG模式為影響單元的FEI文件

同樣，VS模式也包含上述兩種故障類型4種故障模式，即輸出卡死在Selected、Cleared以及Un_Defined和輸出紊亂故障。

綜上，飛行引導系統(tǒng)第一層模型的安全性分析將選用HDG模式和VS模式作為故障影響單元，并定義8個故障模式用以模型擴展及故障分析。

4.4 使用xSAP運行工具對飛行引導系統(tǒng)進行故障分析

4.4.1 模型擴展

使用xSAP將正常NuSMV模型與FEI故障模式進行擴展，如圖13所示，生成兩個文件。其中extended_fgs_firstlevel.smv文件是模型擴展后得到的NuSMV故障擴展模型；fms_fgs_firstlevel.xml文件是FEI故障模式的配置文件，該文件詳細闡述了FEI故障模式文件fgs_firstlevel.fei中每一行代碼的含義以及每一個故障模式的作用。

4.4.2 驗證系統(tǒng)性質(zhì)

對正常NuSMV模型進行模型擴展后得到的擴展模型，其模型中的飛行模式狀態(tài)包含了故障狀態(tài)，因此受故障影響的飛行模式的驗證屬性在進行模型檢驗時會發(fā)生錯誤，模型檢驗器將給出反例路徑。以4.3.2.2小節(jié)中的不變式為例，其在正常的NuSMV模型中屬性驗證為真，而在故障擴展模型中，HDG及VS的狀態(tài)變量有可能會出現(xiàn)輸出卡死和輸出紊亂的故障情況，因此原本驗證為真的屬性在故障擴展模型中驗證為假。具體結(jié)果（部分）如圖14所示。

在正常模型中進行模型檢驗時若出現(xiàn)反例路徑，或表明該反例路徑對應的屬性錯誤，或表明建模錯誤，需要進一步修改屬性或者模型。而在故障擴展模型中進行模型檢驗若出現(xiàn)反例路徑，則表明已成功進行模型擴展。

4.4.3 生成故障樹

故障樹分析是自頂而下的演繹分析，由頂層失效事件（top level event，TLE）逐步建立一個或多個由基本故障事件組成的導致頂事件發(fā)生的所有可能的故障鏈，此故障鏈以樹形結(jié)構(gòu)的形式組成一個故障樹（fault tree）。本次故障樹生成所使用的頂事件為4.3.2.2小節(jié)中不變式的“非”，即：

!(((m_HDG.HDG=Un_Defined)&!(next(m_Select_HDG.result))->next(m_HDG.HDG=Cleared))&(((m_VS.VS=Selected)&next(m_Deselect_VS.result))->next(m_VS.VS=Cleared)));

Fig.13 Result of model extension圖13 模型擴展結(jié)果

Fig.14 Counterexample(Part)圖14 反例路徑（部分）

Fig.15 Result of generating fault tree圖15 生成故障樹的運行結(jié)果

該頂層故障事件表示如果HDG模式處于默認無操作狀態(tài)且其未被選擇，則HDG模式將不會處于未被選擇狀態(tài)；或者，如果VS模式處于被選擇狀態(tài)且被取消選擇，則VS模式將不會處于選擇取消狀態(tài)。

在xSAP工具上使用故障樹生成指令“compute_ft”生成該故障擴展模型的故障樹。運行結(jié)果如圖15所示。

執(zhí)行上述命令可以得到兩個文件，分別為：

（1）extended_fgs_firstlevelevents.txt。該文件包含了能夠?qū)е马攲庸收鲜录l(fā)生的基本故障事件，文件截圖如圖16所示。

圖16 extended_fgs_firstlevelevents.txt

由圖16可知，對于4.3.3小節(jié)定義的8個故障模式，其中只有6個故障模式能夠?qū)е马斒录陌l(fā)生，分別為HDG模式輸出紊亂、HDG模式輸出卡死在Selected、HDG模式輸出卡死在Un_Defined狀態(tài)、VS模式輸出紊亂、VS模式輸出卡死在Selected以及VS模式輸出卡死在Un_Defined狀態(tài)。

（2）extended_fgs_firstlevelgates.txt。gates文件表示故障事件通過邏輯門到達頂事件（邏輯門指“與門”“或門”“非門”），即 extended_fgs_firstlevelevents.txt中的6個故障事件通過“或門”，導致了頂事件的發(fā)生。

生成故障樹文件后，通過xSAP工具中的view_ft命令查看圖形化的故障樹，如圖17所示。從該圖中可以直觀地看出頂事件的發(fā)生由哪些失效事件導致。此故障樹表示，當HDG模式輸出紊亂，或HDG模式輸出卡死在Selected，或HDG模式輸出卡死在Un_Defined狀態(tài)，或VS模式輸出紊亂，或VS模式輸出卡死在Selected，或VS模式輸出卡死在Un_Defined狀態(tài)時，會發(fā)生頂層故障事件。

4.4.4 生成FMEA表

FMEA采用正向推理來評估系統(tǒng)可能的失效影響。本次生成FMEA表依據(jù)的不變式（頂事件的“非”）為：

Fig.17 Fault tree of NuSMV fault extended model圖17 NuSMV故障擴展模型生成故障樹

INVARSPEC((m_When_VS_Button_Pressed_Seen.result)->(m_Deselect_PITCH.result));

此不變式表示的含義為：當選擇垂直速度模式時會導致默認垂直模式即俯仰保持模式被取消。

基于上述不變式的頂事件為：

!((m_When_VS_Button_Pressed_Seen.result)->(m_Deselect_PITCH.result))

生成的一階FMEA表如圖18所示。

圖18表明當VS模式發(fā)生模式輸出卡死在Selected故障或輸出紊亂故障時會導致頂事件的發(fā)生。由此可知若VS模式出現(xiàn)故障不僅對其自身有影響，也會對與其相關聯(lián)的其他飛行模式，如PITCH模式造成巨大影響。

5 小結(jié)

為了提高軟件系統(tǒng)的安全性，基于模型的安全性分析和驗證已經(jīng)成為軟件開發(fā)周期的重要組成部分。文獻[11]詳細介紹了Garmin G1000航空電子系統(tǒng)，并選取了文獻第7章中描述的自動飛行控制系統(tǒng)（automatic flight control system，AFCS）進行分析。文獻[12]利用RSML-e對飛行引導系統(tǒng)需求進行形式化建模。文獻[19]提出了一種將RSML-e模型轉(zhuǎn)換為NuSMV模型的方法，文獻[13]詳細介紹了xSAP工具，在對該工具熟練使用的基礎上，本研究使用該工具對飛行引導系統(tǒng)進行模型擴展和故障分析。

與已有工作相比，本次工作首先針對NuSMV2提出了一種將基于飛行引導系統(tǒng)需求建立的RSML-e模型轉(zhuǎn)換為可進行屬性驗證的NuSMV2模型的方法。其次，從Garmin G1000手冊中推導出與飛行模式相關的安全屬性，并對其進行驗證。最后，根據(jù)飛行引導系統(tǒng)的實際工作情況，設計了兩種飛行模式的失效行為，即模式輸出卡死和模式輸出紊亂，并利用xSAP將兩種失效行為擴展到正常功能的NuSMV模型，生成故障擴展NuSMV模型，用于故障樹分析和FMEA分析。

Fig.18 First order of FMEAtable圖18 一階FMEA表

綜上，通過實際的航空電子系統(tǒng)，進行了系統(tǒng)需求建模、模型轉(zhuǎn)換、模型驗證、系統(tǒng)安全分析和故障分析。從結(jié)果來看，基于MBSA的安全評估方法對于實際系統(tǒng)的驗證是有效的。