安全關(guān)鍵系統(tǒng)需求形式化建模分析實(shí)例研究*

張維珺，胡 軍，李宛倩，陳 朔，石夢(mèng)燁，唐紅英

南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 211106

1 引言

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

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

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

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

2MBSA和形式化模型

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

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

2.2 形式化建模與分析

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

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

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

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

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

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

3.2 安全框架中的核心問題

3.2.1 層次化建模

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

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

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

3.2.2 故障注入機(jī)制

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

Fig.2 Fault injection圖2 故障注入機(jī)制

3.2.3 故障模式及模型擴(kuò)展

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

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

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

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

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

Table 2 Flight modes表2 飛行模式

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

模式輸出卡死故障即為不論該飛行模式被取消或是選擇，其永遠(yuǎn)保持一種狀態(tài)，例如若某一飛行模式卡死在選擇激活狀態(tài)，則無論對(duì)其進(jìn)行取消或選擇操作，該飛行模式永遠(yuǎn)保持選擇激活狀態(tài)，如圖3所示；模式輸出紊亂故障即為該飛行模式最終呈現(xiàn)的狀態(tài)與其被指定的狀態(tài)不符，例如若某一飛行模式輸出紊亂，則對(duì)其進(jìn)行選擇操作，該飛行模式可能處于取消選擇狀態(tài)而非選擇激活狀態(tài)，如圖4所示。針對(duì)某一飛行模式自身出現(xiàn)的故障，不僅對(duì)該飛行模式有影響，也會(huì)對(duì)與該飛行模式相關(guā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)安全性評(píng)估平臺(tái)xSAP

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

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

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

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

4.3 飛行引導(dǎo)系統(tǒng)建模及模型擴(kuò)展

4.3.1 NuSMV建模

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

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

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

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

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

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

4.3.2.1 故障注入

飛行引導(dǎo)系統(tǒng)初級(jí)模型的故障分析重點(diǎn)是對(duì)每個(gè)模式自身的故障進(jìn)行分析，因此僅在NuSMV模型中表示模式狀態(tài)變化的狀態(tài)變量中添加故障事件。選擇航向選擇模式（HDG）和垂直速度模式（VS）作為故障擴(kuò)展單元，對(duì)在HDG和VS上可能發(fā)生的故障行為進(jìn)行擴(kuò)展。在飛行引導(dǎo)系統(tǒng)初級(jí)NuSMV模型的建模過程中，設(shè)定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é)定義的兩種模式故障對(duì)HDG和VS模式進(jìn)行故障注入。

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

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

fault_event_stuck_at_Selected:boolean;

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

fault_event_stuck_at_Cleared:boolean;

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

fault_event_stuck_at_Un_Defined:boolean;

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

--模式的輸出值與正確的輸出值不對(duì)應(yīng)

fault_event_disorderoutput：boolean;

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

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

4.3.2.2 不變式

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

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));

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

4.3.3 FEI故障模式

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

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

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

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

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

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

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

圖9 entering.smv

圖10 during.smv

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

圖10中during.smv文件定義了作用對(duì)象一直處于失效狀態(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)換圖

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

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

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

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

4.4 使用xSAP運(yùn)行工具對(duì)飛行引導(dǎo)系統(tǒng)進(jìn)行故障分析

4.4.1 模型擴(kuò)展

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

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

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

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

4.4.3 生成故障樹

故障樹分析是自頂而下的演繹分析，由頂層失效事件（top level event，TLE）逐步建立一個(gè)或多個(gè)由基本故障事件組成的導(dǎo)致頂事件發(fā)生的所有可能的故障鏈，此故障鏈以樹形結(jié)構(gòu)的形式組成一個(gè)故障樹（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 模型擴(kuò)展結(jié)果

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

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

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

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

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

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

圖16 extended_fgs_firstlevelevents.txt

由圖16可知，對(duì)于4.3.3小節(jié)定義的8個(gè)故障模式，其中只有6個(gè)故障模式能夠?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文件表示故障事件通過邏輯門到達(dá)頂事件（邏輯門指“與門”“或門”“非門”），即 extended_fgs_firstlevelevents.txt中的6個(gè)故障事件通過“或門”，導(dǎo)致了頂事件的發(fā)生。

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

4.4.4 生成FMEA表

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

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

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

此不變式表示的含義為：當(dāng)選擇垂直速度模式時(shí)會(huì)導(dǎo)致默認(rèn)垂直模式即俯仰保持模式被取消。

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

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

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

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

5 小結(jié)

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

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

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

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