基于模型的安全性分析及其在航空發(fā)動(dòng)機(jī)軟件系統(tǒng)上的應(yīng)用

安全性是武器裝備研制、生產(chǎn)、使用和保障的第一要求?；谀Ｐ偷陌踩苑治觯∕BSA）是傳統(tǒng)安全性分析的進(jìn)一步發(fā)展。航空發(fā)動(dòng)機(jī)的設(shè)計(jì)人員與安全分析人員通過(guò)使用相同的系統(tǒng)模型，可避免因系統(tǒng)理解不一致而產(chǎn)生的設(shè)計(jì)分析協(xié)調(diào)問(wèn)題，有助于提高安全性分析的完整性、連續(xù)性與可追溯性。

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

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

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

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

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

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

局限性

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

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

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

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

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

MBSA流程

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

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

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

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

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

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

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

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

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

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

MBSA的優(yōu)勢(shì)

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

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

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

MBSA應(yīng)用于航空發(fā)動(dòng)機(jī)軟件開(kāi)發(fā)

必要性與可行性分析

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

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

分析框架

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

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

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

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

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

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

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

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

結(jié)束語(yǔ)

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