安全性是武器裝備研制、生產(chǎn)、使用和保障的第一要求。基于模型的安全性分析（MBSA）是傳統(tǒng)安全性分析的進一步發(fā)展。航空發(fā)動機的設(shè)計人員與安全分析人員通過使用相同的系統(tǒng)模型，可避免因系統(tǒng)理解不一致而產(chǎn)生的設(shè)計分析協(xié)調(diào)問題，有助于提高安全性分析的完整性、連續(xù)性與可追溯性。

安全性是產(chǎn)品的一種固有屬性，是保障武器裝備使用效能的重要因素。我國自20世紀90年代起，先后頒布了一系列安全性工程技術(shù)和管理規(guī)定，逐步在飛機、火箭、導(dǎo)彈等大型武器裝備系統(tǒng)的研制中推行安全性工程技術(shù)，促進了我國武器裝備安全性工作的迅速發(fā)展。近年來，隨著計算機科學與集成電路技術(shù)的日益盛行，傳統(tǒng)的機械控制越來越多地被嵌入式軟件控制所替代。對于航空航天領(lǐng)域，由于設(shè)計對象高度的系統(tǒng)集成化與深度的軟硬件結(jié)合，如何進行有效的分析與驗證，使嚴苛的安全需求得到保證已成為關(guān)注的焦點。

傳統(tǒng)安全性分析方法及其局限性

傳統(tǒng)安全性分析方法

系統(tǒng)安全性分析過程是傳統(tǒng)安全科學的重要分支，基于系統(tǒng)安全理論的安全性分析方法自20世紀五六十年代誕生以來，一直用于戰(zhàn)略戰(zhàn)術(shù)武器、飛機、核電站等復(fù)雜系統(tǒng)的安全分析?；谙到y(tǒng)安全的通用標準與行業(yè)標準體系日趨成熟且不斷更新改進，其在軍用產(chǎn)品領(lǐng)域主要的標準包括美軍標MIL-STD-882E、英國軍工標準Def Stan 00-56、電子電器產(chǎn)品安全性標準IEC61508等。國內(nèi)軍工領(lǐng)域的主要安全性標準為GJB 900A。此外，在一些特定領(lǐng)域也有各自制定的標準，例如，航空領(lǐng)域系統(tǒng)設(shè)計過程中常用的SAE ARP 4754A和SAE ARP 4761等，最初是為民用機載系統(tǒng)準備，但同樣適用于飛機其他系統(tǒng)，例如發(fā)動機系統(tǒng)及其子系統(tǒng)。以發(fā)動機系統(tǒng)為例，基于SAE ARP 4761的安全性分析流程如圖1所示。

圖1 基于SAE ARP 4761的安全性分析流程

完整的安全性分析流程包括安全性要求的定義與系統(tǒng)安全性要求的驗證，其流程結(jié)構(gòu)符合基于系統(tǒng)工程研制方法的V形結(jié)構(gòu)。系統(tǒng)安全性分析方法按照研制流程分為功能危險分析（FHA）、初步系統(tǒng)安全性分析（PSSA）及系統(tǒng)安全性分析（SSA）三個階段。FHA在設(shè)計研制階段的早期進行，用來識別整機的功能失效情況及功能故障、衰退和功能喪失可能帶來的風險；PSSA以FHA的結(jié)果為輸入，通過安全性分析手段，如故障樹（FTA）等，確定與分系統(tǒng)設(shè)計有關(guān)的危險及部件之間的功能關(guān)系導(dǎo)致的危險及影響，并得到衍生的安全性要求。SSA是在PSSA的基礎(chǔ)上完成的，用以完成系統(tǒng)級安全性的綜合評價。

局限性

在使用基于傳統(tǒng)安全性分析方法進行安全關(guān)鍵系統(tǒng)分析時，由于設(shè)計對象高度的系統(tǒng)集成化以及深度的軟硬件結(jié)合，傳統(tǒng)的安全性分析方法出現(xiàn)了諸多弊端。

首先是系統(tǒng)分析結(jié)果的一致性。傳統(tǒng)的安全性分析需要分析人員在全面了解系統(tǒng)的前提下才能開展安全性分析工作，而在實際分析中，安全性分析人員往往需要投入大量的時間收集系統(tǒng)架構(gòu)信息與系統(tǒng)行為，然后根據(jù)對系統(tǒng)的理解構(gòu)建安全性分析所需要的模型，如FTA等。這種分析的準確性嚴重依賴于分析人員的技術(shù)能力，且高度主觀、易錯，因此衍生出了大量的一致性驗證工作。

其次是分析結(jié)果的重用性。一般而言，不同的研制階段會進行不同程度的安全性分析，隨著研制進度的推進，每一次系統(tǒng)的細化都要進行安全性分析的迭代，系統(tǒng)、部件設(shè)計的改變往往會導(dǎo)致整體安全性分析結(jié)論的變化，例如，系統(tǒng)失效模式與影響分析（FMEA）的變化，從而產(chǎn)生大量重復(fù)性工作。

MBSA流程及其優(yōu)勢

基于模型的安全性分析（MBSA）是在傳統(tǒng)安全性分析的基礎(chǔ)上引入了模型的理念，其核心在于通過計算機實現(xiàn)一部分重復(fù)性的安全性分析工作。在基于模型的研發(fā)過程中，很多研制過程活動，例如，仿真、驗證、測試與代碼生成等，都依賴于一個形式化的系統(tǒng)模型，模型可以用來做各種分析，例如，完整性與一致性分析、模型檢查、定理證明等。

MBSA流程

圖2 加入MBSA方案的安全性分析流程

目前對于MBSA具體應(yīng)該怎樣開展，在技術(shù)上有了一定的研究基礎(chǔ)，但是由于不同研究者采用的技術(shù)不同，所采用的流程也不太相同。英國約克大學利薩戈[1]等人研究了每種MBSA技術(shù)的有效性并進行了對比分析。其中比較有代表性的是美國蘭利研究中心的一份報告，該報告在傳統(tǒng)安全性分析流程中加入了特定的分析理念，擴展總結(jié)了基于模型的安全性分析流程[2-3]，如圖 2所示。

為了支持基于模型的安全性評估，傳統(tǒng)的V形結(jié)構(gòu)需要進行相應(yīng)的修改，以確保安全性分析工作能夠圍繞統(tǒng)一的系統(tǒng)模型展開。這些模型既可用于系統(tǒng)設(shè)計也能用于安全性分析，模型也是系統(tǒng)研制過程中的核心產(chǎn)物。比較典型的MBSA流程包含了形式化定義、名義系統(tǒng)建模、故障建模、模型擴展及安全性分析等流程。

形式化定義安全性需求即是需要驗證的系統(tǒng)安全性屬性，例如航空發(fā)動機不能發(fā)生不可恢復(fù)的空中停車、轉(zhuǎn)子葉片不能斷裂等。定義安全性需求是所有安全性分析工作的第一步。基于MBSA流程的安全性需求的確定與傳統(tǒng)的安全性分析確定需求的方法相同。為了支持自動分析，安全性需求需要通過形式化的符號表示出來。目前學術(shù)界提出了許多描述方法，例如時序邏輯語言CTL/LTL，同樣也可以在構(gòu)建系統(tǒng)模型的建模語言中直接確定安全性要求[4]。

名義系統(tǒng)建模名義系統(tǒng)模型是指系統(tǒng)研發(fā)工程師和安全性工程師共同使用的明確的系統(tǒng)模型。名義模型中的系統(tǒng)行為用形式化語言表示，目前可采用的形式化配置語言種類繁多，支持圖形或者文本等多種描述。例如，Matlab綜合仿真環(huán)境Simulink/Stateflow，安全關(guān)鍵系統(tǒng)綜合驗證平臺SCADE及相應(yīng)支持語言——時序文本語言Lustre，基于AltaRica的分析驗證平臺Cecilia OCAS、Simfia等。

故障建模故障模型包含的信息主要包括各種系統(tǒng)部件（包括數(shù)字控制器與機械系統(tǒng)）的故障方式。它定義了通用失效模式的行為，例如不確定、翻轉(zhuǎn)、死鎖等。故障模型同時也說明了故障的觸發(fā)條件與失效時間，以及更復(fù)雜的故障行為，例如故障傳播、條件故障（從屬故障）等。借助于系統(tǒng)模型，可以構(gòu)造不同類型的數(shù)字故障、機械故障、時間故障等。當前的MBSA技術(shù)中利用Simulink/Stateflow或SCADE來描述故障行為的研究較多。

模型擴展將故障模型加入到名義系統(tǒng)模型中，描述系統(tǒng)在各種故障條件下的行為，得到的模型稱作擴展系統(tǒng)模型。目前有兩種方式將故障信息加入到系統(tǒng)模型中：第一種方式是構(gòu)建一個獨立于系統(tǒng)模型的故障模型，自動將兩種模型合并用于分析，但這種建模方式在描述連續(xù)系統(tǒng)時存在一定的局限性，并且對系統(tǒng)信息的需求較大；第二種建模思路是直接構(gòu)建失效情況下的行為，例如失效傳播與轉(zhuǎn)化符號（FPTN）、分層危險起因與傳播研究（HiP-HOPS）等失效邏輯建模方法。在名義系統(tǒng)模型中加入了故障信息后，即得到了待驗證的擴展模型。

安全性分析對模型開展安全性分析是MBSA的關(guān)鍵環(huán)節(jié)。傳統(tǒng)的安全性分析是通過模擬手段完成，即所謂的仿真方法，除此之外，計算機領(lǐng)域形式化方法的研究使模型檢查、定理證明等新型分析方法在模型的分析中廣泛普及。

采用仿真策略的安全性分析方法就是通過給所構(gòu)建的模型施加激勵信號或者外部數(shù)據(jù)，演繹系統(tǒng)正?；蚴У膭幼髋c場景，判斷系統(tǒng)安全性要求是否都得到了滿足。采用仿真方法進行安全性分析的優(yōu)勢是原理簡單易于實現(xiàn)。但仿真往往只能證明系統(tǒng)在預(yù)期條件下做了預(yù)期的事，并不能證明系統(tǒng)是否會做預(yù)期以外的事，因此仿真存在非完備性的缺點。目前MBSA研究領(lǐng)域采用仿真方法開展安全性分析的研究不多，在工程中更傾向于采用形式化方法（Formal Method）驗證安全性需求是否被滿足。

形式化方法最初是用在軟件工程領(lǐng)域，主要目的是通過精確的數(shù)學語言來描述系統(tǒng)的結(jié)構(gòu)和運行過程，它是設(shè)計與編寫程序的出發(fā)點，也是驗證程序是否正確的最重要依據(jù)。在模型建立完成之后，形式化方法可以被分為兩類：一是模型檢查，二是定理證明。在這兩類方法中，模型檢查方法相對成熟[5]，它是將原始設(shè)計表述成特定的模型，將要驗證的性質(zhì)用時態(tài)邏輯語言描述，通過遍歷模型狀態(tài)空間檢驗需求是否滿足。模型檢查的優(yōu)點是分析過程全自動且無須人機交互，當判斷性質(zhì)不能滿足時可以給出反例以定位設(shè)計錯誤。目前存在許多成熟的模型檢查工具，例如貝爾實驗室的軟件與協(xié)議驗證工具SPIN、卡耐基梅隆大學的符號模型驗證工具SMV及其升級版本NuSMV。由于模型檢查有著檢測效率高且能夠判斷預(yù)期之外的故障是否發(fā)生的優(yōu)勢，因此基于模型檢查的MBSA是目前進行模型安全性分析的主流。

MBSA的優(yōu)勢

基于以上分析，相較于傳統(tǒng)安全性分析方法，MBSA具有以下優(yōu)點。

首先，系統(tǒng)設(shè)計人員與安全分析人員能夠使用相同的系統(tǒng)模型，從而避免了由于系統(tǒng)理解不一致而產(chǎn)生的設(shè)計分析協(xié)調(diào)問題，有助于提高安全分析的完整性、連續(xù)性與可追溯性。

其次，基于模型開展安全性分析，可以利用現(xiàn)有的自動分析算法（形式化驗證方法）通過計算機實現(xiàn)自動的安全性分析，在精準、高效、完備的基礎(chǔ)上，也盡可能地減少安全分析人員的重復(fù)性工作，降低設(shè)計成本，同時也提高安全分析的質(zhì)量。

MBSA應(yīng)用于航空發(fā)動機軟件開發(fā)

必要性與可行性分析

航空發(fā)動機作為復(fù)雜程度極高的關(guān)鍵系統(tǒng)，其安全性關(guān)系到發(fā)動機乃至飛機的使用壽命，甚至威脅到乘客及飛行員的人身安全。世界各國適航當局以確保安全為目的，頒布了各類適航規(guī)章、審定規(guī)范。我國借鑒美國聯(lián)邦航空局（FAA）頒布的FAR33《航空發(fā)動機適航標準》頒布了中國民用航空規(guī)章CCAR33《航空發(fā)動機適航規(guī)定》，CCAR33的第33.75條款是專門針對發(fā)動機及其子系統(tǒng)安全性要求提出的，明確指出申請人必須對發(fā)動機及其控制系統(tǒng)進行安全性分析，以確保航空發(fā)動機的安全水平[6]。但當前國際上通常使用的分析方法仍是將民用飛機系統(tǒng)安全性分析方法直接運用到航空發(fā)動機上，導(dǎo)致航空發(fā)動機的安全性分析仍具有高度的主觀性，因此，將MBSA應(yīng)用到航空發(fā)動機上是十分必要的。

基于模型的航空發(fā)動機安全性分析，可以提供統(tǒng)一的系統(tǒng)模型，解決了因缺少統(tǒng)一架構(gòu)模型導(dǎo)致無法進行完備的安全性分析的難題，并使得安全性分析隨著研制模型的不斷迭代而更具有連續(xù)性、一致性與可追溯性。因此，將MBSA應(yīng)用于航空發(fā)動機是可行的。

分析框架

圖3 基于模型的航空發(fā)動機軟件系統(tǒng)安全性分析框架

現(xiàn)階段MBSA的應(yīng)用主要集中在機載系統(tǒng)，且現(xiàn)有研究仍處于底層部分軟件系統(tǒng)，鮮見在航空發(fā)動機整機系統(tǒng)上的應(yīng)用。在航空發(fā)動機軟件開發(fā)領(lǐng)域，已有基于模型開發(fā)的研究案例，即利用較為成熟的SCADE平臺，將成熟的Simulink模型轉(zhuǎn)換成SCADE模型，在SCADE平臺中進行模型驗證并生成代碼，最后進行集成驗證[7]。因此，在航空發(fā)動機軟件系統(tǒng)率先進行MBSA的應(yīng)用是現(xiàn)實可行的。目前工程研究人員廣泛采用的模型構(gòu)建及分析工具是Simulink與SCADE。SCADE專注于高安全性系統(tǒng)和嵌入式軟件的集成開發(fā)，提供了多種接口，支持跨平臺的聯(lián)合開發(fā)。在與Simulink的聯(lián)合開發(fā)方面，SCADE提供了Simulink Gateway和Simulink Wrapper，支持兩者交互式開發(fā)。其中，SCADE Simulink Gateway包括Simulink Translator和Stateflow Importer兩個模塊，能將Simulink模型轉(zhuǎn)換成SCADE模 型。Simulink Wrapper可 將SCADE模型集成到Simulink模型中并在Simulink環(huán)境下進行聯(lián)合仿真。目前, GE公司、羅羅公司、普惠公司都用SCADE作為MBD的開發(fā)環(huán)境。

因此，本文嘗試提出基于SCADE平臺對航空發(fā)動機控制系統(tǒng)的軟件部分應(yīng)用MBSA的框架，如圖3所示，試圖為航空發(fā)動機安全性分析與驗證提供一種全新的思路。

首先提出航空發(fā)動機控制系統(tǒng)的軟件安全性需求，包含三個來源：一是航空發(fā)動機FHA的結(jié)論；二是對航空發(fā)動機不同層級（整機級、系統(tǒng)級、部件級）FTA及FMEA的結(jié)論；三是前一研制階段模型檢查得到的結(jié)論。以上分析結(jié)果是以直白的文字語言表達的，例如，航空發(fā)動機控制系統(tǒng)的軟件部分不能發(fā)生進程死鎖，需要將其應(yīng)用時態(tài)邏輯進行形式化表達，使其能夠作為模型檢查的輸入語言。通常，時態(tài)邏輯按照對系統(tǒng)時間的假設(shè)分為線性時態(tài)邏輯（LTL）和計算樹邏輯(CTL) ，由于兩種時態(tài)邏輯的描述方式與描述能力存在差異，需要依據(jù)安全性需求的特點選擇合適的時態(tài)邏輯。得到安全性需求的形式化表達后，應(yīng)用SCADE或Simulink進行航空發(fā)動機名義系統(tǒng)建模，來描述控制系統(tǒng)正常工作情況下的系統(tǒng)行為。安全分析人員在得到航空發(fā)動機名義系統(tǒng)模型后，再應(yīng)用SCADE或Simulink將失效模式進行建模，并注入到名義模型中，相當于對名義系統(tǒng)內(nèi)的正常行為添加行為偏差，獲得擴展的系統(tǒng)模型。將該擴展模型在SCADE平臺中進行模型檢查，通過自動遍歷系統(tǒng)所有狀態(tài)，驗證是否存在進程死鎖的可能，若平臺輸出TRUE則說明滿足控制系統(tǒng)軟件安全性要求，若輸出FLASE則模型檢查將輸出反例，即一次或多次故障的行為軌跡，進而可以幫助航空發(fā)動機安全性分析人員推演進程死鎖的事故路徑。

關(guān)鍵技術(shù)

雖然將MBSA應(yīng)用于航空發(fā)動機上是必要且可行的，但需要克服一些關(guān)鍵技術(shù)難題以求得進一步發(fā)展。

一是如何建立高保真模型。MBSA的核心是模型，模型的精確程度將決定著安全性分析的精確程度。航空發(fā)動機包含大量的熱、氣動、結(jié)構(gòu)、強度等參數(shù)，如何使航空發(fā)動機名義模型與失效模型最大程度地接近發(fā)動機實際狀態(tài)，對提高安全性分析的準確性具有重要意義。

二是如何轉(zhuǎn)換安全性分析結(jié)論?，F(xiàn)有基于模型的形式化驗證的結(jié)論通常是用計算機語言描述的，語義難以理解且不能作為工程中安全性審查的結(jié)論。如何能將形式化驗證的結(jié)果自動的轉(zhuǎn)換為傳統(tǒng)安全性驗證結(jié)論（如FTA、FMEA等），找到模型檢查與傳統(tǒng)安全性分析工作的橋接，對完善MBSA流程具有重要意義。

結(jié)束語

MBSA作為當前國際安全性領(lǐng)域的研究熱點，利用模型分析不僅可以提高安全性分析的準確性和效率，也為開展基于模型的各項智能化技術(shù)提供了良好的接口。對于航空發(fā)動機這一復(fù)雜關(guān)鍵系統(tǒng)，借助已有的研究經(jīng)驗對MBSA框架下的各項技術(shù)進行深入的應(yīng)用研究，不僅能夠為航空發(fā)動機安全性分析提供研究基礎(chǔ)和技術(shù)積累，同時也將對提高航空發(fā)動機的安全性、可靠性帶來巨大的工程價值。