基于模型的安全性分析及其在航空發動機軟件系統上的應用

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

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

傳統安全性分析方法及其局限性

傳統安全性分析方法

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

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

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

局限性

在使用基于傳統安全性分析方法進行安全關鍵系統分析時，由于設計對象高度的系統集成化以及深度的軟硬件結合，傳統的安全性分析方法出現了諸多弊端。

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

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

MBSA流程及其優勢

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

MBSA流程

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

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

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

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

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

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

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

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

采用仿真策略的安全性分析方法就是通過給所構建的模型施加激勵信號或者外部數據，演繹系統正常或失效的動作與場景，判斷系統安全性要求是否都得到了滿足。采用仿真方法進行安全性分析的優勢是原理簡單易于實現。但仿真往往只能證明系統在預期條件下做了預期的事，并不能證明系統是否會做預期以外的事，因此仿真存在非完備性的缺點。目前MBSA研究領域采用仿真方法開展安全性分析的研究不多，在工程中更傾向于采用形式化方法（Formal Method）驗證安全性需求是否被滿足。

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

MBSA的優勢

基于以上分析，相較于傳統安全性分析方法，MBSA具有以下優點。

首先，系統設計人員與安全分析人員能夠使用相同的系統模型，從而避免了由于系統理解不一致而產生的設計分析協調問題，有助于提高安全分析的完整性、連續性與可追溯性。

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

MBSA應用于航空發動機軟件開發

必要性與可行性分析

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

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

分析框架

圖3 基于模型的航空發動機軟件系統安全性分析框架

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

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

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

關鍵技術

雖然將MBSA應用于航空發動機上是必要且可行的，但需要克服一些關鍵技術難題以求得進一步發展。

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

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

結束語

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