一個基于形式化方法的系統安全性建模分析實例研究

石夢燁，胡 軍，陳 朔，唐紅英，王立松

(南京航空航天大學 計算機科學與技術學院，南京 211106)(軟件新技術與產業化協同創新中心，南京 211106)

1 引 言

近年來，隨著各類安全關鍵系統[1，2]功能的不斷增強和需求的日益增加，對傳統的系統工程開發和安全性分析技術提出了很大的挑戰.基于模型的安全性分析[3，4](Model Based Safety Analysis，MBSA)是近年出現的一類對復雜系統建模并基于系統模型實現自動或半自動化的安全分析及驗證的技術方法.MBSA已成為系統建模和分析領域的一個熱點研究問題.

MBSA方法是形式化方法在安全關鍵系統的應用，旨在系統復雜性上升的同時保持或提高其安全性水平.它用于支持系統設計層級的分析，包括三個關鍵要素[5]：

1)對整個系統進行形式化模型的構建，其中模型是組件的集合；

2)對模型進行定性和定量分析，將可能存在的安全問題設置成一系列故障模式；

3)對擴展模型進行形式化安全分析.

國際汽車工程師協會(Society of Automotive Engineers，SAE)架構分析與設計語言(Architecture Analysis and Design Language，AADL)[6，7]是一種形式化建模語言，通過可擴展的標記符、工具框架和精確的語法語義，用于設計和分析復雜系統的軟件和硬件架構及其性能關鍵特性.

本文主要工作以AADL的子集SLIM為建模語言，基于xSAP(The eXtended Safety Assessment Platform)為安全性分析平臺的形式化驗證方法[8]，以AIR6110中的機輪剎車系統[9]為實例，對其進行安全性建模和分析.通過一個實例展現了面向SLIM模型進行安全性分析和形式化驗證的過程.本文的結構安排如下：第二節，主要介紹了MBSA框架、形式化方法在MBSA的應用、建模語言SLIM，和驗證工具NuSMV[10，11]；第三節，簡要介紹了AIR6110標準和機輪剎車系統，并詳細給出了用SLIM對其進行形式化建模的過程以及建模時遇到的問題，設計了多種類的故障模式并進行模型擴展；第四節對建立的機輪剎車模型進行分析并展現了驗證結果；最后總結全文.

2 基于形式化方法的安全性分析方法架構

2.1 MBSA框架

MBSA方法學是一種系統設計工程師和安全工程師共享使用基于模型的開發過程創建的公共系統模型的方法[12].如圖1所示，在設計階段通過形式化語言描述復雜系統的行為架構，來構造一個通用的需求模型；在安全性分析階段中基于所建立的系統模型來進行失效行為的語義擴展，并盡可能的自動化生成系統失效行為的最小割集故障樹[13]和失效序列.

圖1 MBSA方法框架Fig.1 MBSA method framework

總體上來看，MBSA的總目標是：1)提供一個可公用且嚴格定義的系統模型，確保隨著系統架構的發展，安全分析結果是最新的；2)通過將傳統的安全分析過程與基于模型的開發活動相結合，允許開發早期可以進行安全評估，降低因系統復雜度提高造成的成本增加并提高安全分析過程的質量；3)系統開發工程師和系統安全工程師可以通過公用的形式化模型進行溝通，便于對系統的理解.

2.2 MBSA中的形式化方法

形式化方法[5，14]是將數理和邏輯方法(如邏輯、自動機、圖論)運用在計算機工程領域，通過借助形式化語言，去構建計算機系統的數學模型并進行模型推理和驗證.它的應用領域是多方面的：首先使用形式化語言去描述符合語法語義規則的完整的系統模型；其次使用形式化分析技術和形式化工具分析系統模型；最后，形式化方法滲透在系統開發過程的各個階段，包括需求分析、設計、實現.它可以用來引導安全關鍵系統的開發過程，盡早發現每個階段的缺陷問題.

在系統的開發過程中，采用具有嚴格語法語義定義的形式化建模語言可以建立精確且公用的數學模型.在安全評估過程中，采用形式化分析技術可以對公用的系統模型的擴展形式進行分析和驗證，來發現模型中可能存在的安全問題.采用形式化工具可以自動化驗證過程，減少人工檢查的高成本并減少錯誤.因此形式化方法在MBSA方法中極為重要[15，16].

MBSA的起點和重點是創建公用的需求模型.在本文工作中選用的是系統級集成建模語言(System-Level Integrated Modeling language，SLIM)對系統進行需求規約.SLIM是AADL的精化，一個完整的SLIM系統規范由三部分組成，即正常行為的描述、錯誤行為的描述以及描述錯誤行為如何影響正常行為的故障注入規范.NuSMV(New Symbolic Model Verifier)是一個符號模型檢驗工具，支持先進的模型檢驗技術[17]，基于BDD(Binary Decision Diagrams)和SAT(Satisfiability)針對CTL(Computation Tree Logic)[10]和LTL(Linear Temporal Logic)[18]時態邏輯進行驗證，可用于對SLIM建立的需求模型進行分析.

3 AIR6110標準中的機輪剎車系統的實例建模研究

3.1 AIR6110標準和WBS概述

在本文的工作中，選擇了在SAE的AIR6110標準中所給出的一個典型的安全關鍵系統實例展開研究，這是一個航空領域中的飛機機輪剎車系統的系統規范和安全性分析實例.AIR6110文件由SAE于2011年發布，SAE AIR6110的全稱是“連續飛機/系統開發過程示例”，其中機輪剎車系統(WBS)的開發和安全性分析完全遵循工業標準ARP4754A—“民用飛機和系統發展指南”[19]和ARP47611—“進行民用機載系統和設備安全評估程序的指南和方法”[20]中的要求.ARP4754和ARP4761是目前航空電子領域的開發和安全評估過程的工業標準.

圖2 機輪剎車系統模型概觀Fig.2 Overview of the wheel brake system model

在AIR6110所給出的這個實例系統中，主要描述了WBS的系統框架結構和功能要求，其中，WBS由制動系統控制單元(Brake System Control System，BSCU)和液壓調節系統組成.圖2是機輪剎車系統的模型概觀.

BSCU是系統中的數據處理組件，收集來自踏板、機輪速度等信息作為輸入，使用內部的命令單元進行計算并向液壓調節系統輸出不同命令：傳輸到液壓調節系統正常線路的控制命令，傳輸到液壓調節系統備用線路的控制命令，對關閉閥和選擇閥進行調控的開關命令.BSCU還包含監控單元，主要用于監控命令單元的狀態.默認情況下，BSCU使用第一組命令和監控設備.當監控設備發出錯誤警報，則由選擇設備自動切換成備用組.

液壓調節系統用于對機輪進行供壓，分為正常線路和備用線路.正常線路包括綠色液壓泵、關閉閥、限量閥；備用線路包括藍色液壓泵、隔離閥、蓄壓泵、防滑閥、人工剎車裝置.正常線路由綠色液壓泵供壓，備用線路處于待機狀態，由藍色液壓泵供壓.當藍色液壓泵失效時，由用于驅動剎車制動器的蓄壓泵支持.選擇閥為兩條線路共有，起線路切換功能.當正常線路失效，則轉換至備用線路.若備用線路也失效，則由人工剎車裝置額外提供液壓.

3.2 WBS的形式化建模

上一節用自然語言概要描述了AIR6110標準中的WBS系統架構和功能，接下來在本節中將采用SLIM對WBS系統的功能進行形式化建模.本文將機輪剎車系統按表1所示分層結構建模.

表1 WBS分層模型整體框架圖
Table 1 Overall framework of WBS hierarchical model

模型層級系統包含的子組件BSCU子系統第一層WBS液壓調節系統監控器lru1、第二層BSCU子系統lru2、選擇設備綠色液壓泵、藍色液壓泵、第二層液壓調節系統關閉閥、蓄壓泵、隔離閥、選擇閥、限量閥、防滑閥、人工剎車裝置第三層LRU監控單元命令單元

給出液壓調節系統的選擇閥的SLIM描述如圖3所示，其他部件可以通過類似方法得到其對應的SLIM代碼模塊，在此不再贅述.

首先設置端口，選擇閥的輸入端口有來自蓄壓泵的液壓accumulator_input，來自正常線路的液壓green_input，來自備用線路的液壓blue_input，來自monitor的事件switch，以及來自BSCU的select_alternate.輸出端口有green_out，blue_out.其中，accumulator_input、green_input和blue_input的數據類型是intRange，范圍是[0…10]，初始值為5，select_alternate是布爾型端口，初始值為false.

共設置四種模式：select_green、select_blue、select_accu、fail，初始模式是select_green.圖3設置了7種轉換.

第1個轉換說明，如果收到的數據端口綠色液壓值大于等于5，則說明使用正常線路，那么令液壓值等于輸入的綠色液壓值.

圖3 選擇閥建模代碼
Fig.3 Selector modeling

第2、3、4這三個轉換說明如果收到的綠色液壓值green_input小于5，則選擇備用線路；收到switch事件，則系統從select_green轉變為select_blue，即選擇備用線路；當選擇閥收到來自BSCU的select_alterate值為true，即表示當前正常線路出現了問題，則使用備用線路，令選擇閥的輸出液壓值為藍色液壓值.

第5、6、7這三個轉換說明，如果收到的來自藍色液壓泵的液壓值≥5，則使用備用線路，并令選擇閥的輸出液壓值為藍色液壓值；若收到的藍色液壓值<5，而蓄壓泵的液壓值≥5，則使用蓄壓泵的液壓值；當蓄壓泵的液壓值也小于5，說明蓄壓泵也出現問題，則失敗.

在面對AIR6110標準建模的過程中，我們發現了一些在AIR6110標準文檔中尚未清楚闡述的地方，如：在標準的文字描述中給出“正常線路的液壓值會作為反饋傳輸到BSCU中.當該反饋值小于指定的值時，就類似于一個指示信號，指示正常線路失效.這種情況下，BSCU會產生一個命令，將關閉閥關閉.”并未說明BSCU的命令如何傳到該閥？此外，AIR6110標準中的Arch4架構顯示，監控單元有一根連著關閉閥的線，它是否可以用來控制閥門?

由此可見，自然語言存在無法闡述清楚系統需求或者存在二義性問題.而形式化方法是基于形式化語言的，具有非常精確的語義，因此可以明確地解釋系統出現的問題.在進行形式化建模的時候，新的系統除去了由液壓調節系統指向BSCU的液壓反饋值.建模時，在BSCU系統中單獨建了一個select系統，它接受來自于監控單元的數據，用于判斷是否使用備用液壓，它的輸出select_alternate會傳到關閉閥中.如果select_alternate為true，則說明當前正常線路出現了問題，那么則關閉關閉閥.

另外，在標準文字表達中出現：“防滑閥也能對液壓進行調整”，實際系統中如何體現對液壓的修改？

由于標準中記載的防滑閥和限量閥的功能是：“防滑閥遵循BSCU傳出的命令去控制制動器的液壓，它用于限制制動器的液壓管路壓力以防止機輪鎖定.”以及“當飛行員或自動剎車系統測量到壓力超過滑行輪胎所需的壓力時，通過降低制動壓力來優化制動.限量閥根據BSCU傳來的控制命令，對液壓調節系統的液壓值進行調節，并把調節后的值傳輸到機輪.”也就是說，防滑閥和限量閥的主要功能是降低制動壓力.所以，在使用SLIM進行建模的時候，設置它們的壓力變化為不變和下降.相應的，BSCU產生的命令為down和nochange.

3.3 用xSAP對WBS模型故障擴展

由于上一節中建立的模型是假設系統在理想情況下運行.而實際情況下，安全分析需要考慮到可能發生的不同故障以及系統組件可能出現故障的各種方式，因此必須使用系統的故障行為來增強基于模型的開發中捕獲的正常系統行為.xSAP支持基于庫的故障模式定義，可以對正常的系統功能行為進行模型擴展，擴展后的模型通過安全性分析來評估存在故障的系統行為.

3.3.1 故障設置

在此以液壓調節系統中的閥類為例設計故障.對關閉閥設置了三種不同的狀態：OK，Dead，Stuck_at_zero.OK表示初始狀態，Dead是失效狀態，失效的原因來自于內部軟件錯誤事件internal_error.Stuck_at_zero是卡死狀態，當出現錯誤事件stuck_at_zero時，pump會從OK變成Stuck_at_zero.這種情況下，無論輸入的液壓值是多少，輸出的液壓值都為0.

具體實現中，設置兩個故障事件，internal_error和stuck_at_zero.internal_error是液壓錯誤事件，stuck_at_zero是卡死故障，表示卡死在液壓值0.接下來定義轉換，分別定義了以下轉換：

1)OK-[Internal_error]->Dead；

2)OK-[stuck_at_zero]->Stuck_at_zero.

系統初始時處于OK狀態，當遇到故障事件internal_error，會從OK轉為Dead.當遇到卡死事件stuck_at_zero，會從OK轉為Stuck_at_zero.

3.3.2 故障擴展

上一節中所設計的系統故障行為是從安全性分析的視角來進行設計的，還需要進一步將這些可能的故障信息與正常的系統功能行為合并在同一個模型中進行完整的系統分析.這種合并是通過在模型層的故障注入方式來實現的.

故障注入描述了錯誤發生對系統正常行為的影響.更具體地說，它指定當關聯的錯誤模型進入特定錯誤狀態時組件實現中的數據元素經歷的值更新.

在本實例的研究中使用xSAP對模型進行擴展，選擇三個故障注入，分別是:1)電源2發生故障；2)主模式BSCU系統中的監控單元出現錯誤；3)液壓調節系統中的綠色液壓泵發生錯誤.

4 機輪剎車模型的安全性分析

形式化分析工具可以用來對建立的模型進行安全性分析.以xSAP為核心的COMPASS(Correctness，Modeling，and Performance of Aerospace Systems)分析[21，22]包括對系統進行形式化建模，即建立SLIM模型；對系統進行定性分析并設計安全屬性；考慮系統可能存在的失效行為并進行語義擴展和分析.COMPASS的輸入為根據系統架構建立的正常模型和設置的故障模式，以及一組表示系統規約的屬性.輸出為反例路徑、故障樹、FMEA表[5，23]、FDIR[24]等可視化界面.

4.1 模型的動態仿真

模型模擬主要用于檢查系統功能的正確性.圖4是模型的部分運行圖形，在此選擇運行的步長為20.軌跡由一個表格組成，其中第一列提供了模型元素的名稱，在其他列中顯示了該元素在每個步驟的值.布爾條紋顯示為具有兩個值的波形，其中high為true，low為false.

圖4 對擴展的WBS系統進行動態仿真Fig.4 Dynamic simulation of extended WBS systems

通過圖4中的模擬結果可以發現，由于主模式的監控單元發生了invalidReport錯誤，導致判斷監控單元是否有效的輸出valid的值為false，該故障作為故障傳播進入BSCU中的select_Alternate.監控器收到來自BSCU中監控器的錯誤，引發switch事件，switchBSCU和alarmBSCU變為true，switch事件傳入BSCU，導致BSCU系統從Primary轉為Backup.

4.2 模型檢測

模型檢測用于根據一個或多個屬性檢查SLIM模型.通過將指定的屬性描述為時態邏輯公式并使用特定的符號算法進行狀態空間的智能搜索來確定屬性是真是假.若屬性為假，則生成反例軌跡以顯示違反該屬性的模型的執行軌跡來進行深入的進一步分析.否則，顯示屬性正確.共設計并驗證了15條屬性，其中6條正確，9條錯誤，耗時8.36秒.

圖5 模型檢查得到錯誤屬性的反例Fig.5 Model check gets a counterexample of the wrong attribute

在此選取其中兩個進行說明.首先對屬性“AG(valid=false and bscu.mode=mode：Backup-> AF alarmBSCU)has been found false.”進行驗證，該屬性的含義為：無論何時原子命題“valid=false and bscu.mode=mode：Backup”成立，它最終一定會被響應alarmBSCU.如圖5所示，結果顯示該CTL屬性錯誤并給出反例路徑.

接下來對CTL屬性“AG(bscu.mode=mode：Backup and bscu.valid=false-> EF alarmBSCU)has been found true”進行檢查，它的含義是當BSCU當前的模式是Backup，并且valid值為false，則表明BSCU系統已經是失效，可能會響應警報alarmBSCU.在模型中，該CTL屬性成立.

4.3 形式化模型的安全性分析

經典的系統安全性分析方法有故障樹分析(Fault Tree Analysis，FTA)和故障模式和影響分析(Fault Mode and Effect Analysis，FMEA).FTA是一種自頂向下的方法，它通過考慮所分析系統的意外行為，自上而下分析追蹤直到找出所有故障模式.FMEA則是一種自底向上的方法，它通過考慮給定的危害的起因，分析其可能的安全后果.

4.3.1 故障樹分析

在此選擇屬性“bscu fail twice”作為頂層故障事件(Top Level Event，TLE)進行故障樹分析的說明，它的不定式是“bscu.valid=false and bscu.mode=Backup”，含義是當前BSCU子系統處于備用模式且輸出端口valid的值為false，即兩個監控命令單元都失效.這種情況下，說明整個BSCU子系統已經失效.使用COMPASS中生成故障樹的功能，生成對應的故障樹.故障樹顯示如何達到與TLE相對應的狀態，即通過AND和OR門連接可能導致TLE的基本事件序列(故障).

通過運行故障樹，頂層事件“bscu fail twice”得到兩個文件：wbs_000001.flt_events和wbs_000001.flt_gates.其中wbs_000001.flt_events包含三個基本事件，分別是：

1)E2：bscu.lru1.mon._errorSubcomponent.#invalidReport

它表示BSCU子系統的lru1子系統的監控單元發生了invalidReport故障.

2)E5：power._errorSubcomponent.#close

它表示電源組件發生了close故障.

3)E6：power._errorSubcomponent.#depleted

它表示電源組件發生了deplted故障.

圖6 “bscu fail twice”的故障樹Fig.6 Fault tree of “bscu fail twice”

圖6是導致頂層事件“bscu fail twice”發生的故障樹.如圖所示，在這個故障樹中有兩個分支引起故障：一個分支是E2和E5，它們通過與門連接，一起導致事件fault_cfg_1的發生；另一個分支是E2和E6，也通過與門連接，導致事件fault_cfg_2的發生.該故障樹的邏輯公式表示為：(E2∧E5)∨(E2∧E6).

故障樹的最小割集(Minimum cutset，MCS)[25]是導致TLE發生的組件故障的最小組合，它代表對TLE的更簡單的解釋.TLE是MCS的析取，每個割集則是相應基本故障事件的合取.“bscu fail twice”的MCS共兩個，為E2∧E5和E2∧E6.

4.3.2 故障模式和影響分析

FMEA以表格的形式顯示了可能導致一個或多個故障狀態的所有可能的事件組合.本次生成FMEA表依據的屬性為：“bscu.mode=mode：Backup”.此屬性表示的含義是：BSCU主模式失效.結果表明為了引發事件“bscu.mode=mode：Backup”，故障事件組合有以下幾種情況.

1)基數為1的1個組合：

即“bscu.lru1.mon._errorSubcomponent.# invalidReport=True”.它代表BSCU子系統中的lru1的監控單元發生故障invalidReport.

2)基數為2的4種組合：

即“(hydr.green_pump._errorSubcomponent.# hydraulicError=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True)”.它代表液壓調節系統的綠色液壓泵出現故障hydraulicError并且BSCU子系統中的lru1的監控單元發生故障invalidReport.

以及“(hydr.green_pump._errorSubcomponent.# stuck_at_zero=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True)”.它代表液壓調節系統的綠色液壓泵出現故障stuck_at_zero并且BSCU子系統中的lru1的監控單元發生故障invalidReport.

以及“(power._errorSubcomponent.# close=True &bscu.lru1.mon._errorSubcomponent.#invalidReport=True)”.它代表電源組件出現故障close，并且BSCU子系統中的lru1的監控單元發生故障invalidReport.

以及“(power._errorSubcomponent.# depleted=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True)”.它代表電源組件出現depleted的故障，并且BSCU子系統中的lru1的監控單元發生故障invalidReport.

3)基數為3的4種組合：

即“(power._errorSubcomponent.# close=True &(bscu.lru1.mon._errorSubcomponent.#invalidReport=True &hydr.green_pump._errorSubcomponent.#hydraulicError=True))”.它代表電源組件出現故障close，BSCU子系統中的lru1的監控單元發生故障invalidReport，以及液壓調節系統的綠色液壓泵出現故障hydraulicError.

以及“(power._errorSubcomponent.#depleted=True &(bscu.lru1.mon._errorSubcomponent.#invalidReport=True &hydr.green_pump._errorSubcomponent.# hydraulicError=True))”.它代表電源組件出現故障depleted，BSCU子系統中的lru1的監控單元發生故障invalidReport，并且液壓調節系統的綠色液壓泵出現故障hydraulicError.

以及“(power._errorSubcomponent.#depleted=True &(hydr.green_pump._errorSubcomponent.# stuck_at_zero=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True))”.它代表電源組件出現故障depleted，液壓調節系統的綠色液壓泵出現故障stuck_at_zero并且BSCU子系統中的lru1的監控單元發生故障invalidReport.

以及“(power._errorSubcomponent.#close=True &(hydr.green_pump._errorSubcomponent.#stuck_at_zero=True &bscu.lru1.mon._errorSubcomponent.#invalidReport=True))”.它代表電源組件出現故障close，BSCU子系統中的lru1的監控單元發生故障invalidReport并且液壓調節系統的綠色液壓泵出現故障stuck_at_zero.

5 相關工作與小結

為了提高安全關鍵性系統的安全性，使用基于模型的安全評估技術對復雜系統進行形式化建模和安全性分析受到了學術界和工業界的關注.文獻[7]提供了AADL的語法，介紹了它的接口和具體實現，并通過示例的講解為AADL對大型系統的建模提供了思路.文獻[9]詳細介紹了AIR6110標準中的機輪剎車系統(WBS)，描述了它的架構以及功能需求，本文選擇了它的最新架構圖進行建模和分析.

與已有工作相比，本研究主要工作為：將WBS分為整體層、子系統層及設備層，采用AADL的子集SLIM對其進行系統級建模，充分考慮了組件之間的交互；針對文獻[9]未說明BSCU的命令如何傳到關閉閥從而對關閉閥進行控制，形式化建模時，在BSCU系統中單獨建了一個select系統，它接受來自于監控單元的數據，用于判斷是否使用備用液壓，它的輸出select_alternate會傳到關閉閥從而對關閉閥進行控制；考慮WBS可能發生的故障并設計一系列故障模式，選擇指定故障與系統正常功能行為合并為擴展模型，從而進行安全性分析.

盡管本文的研究結果論證了基于模型的安全分析方法對于提高安全關鍵性系統的安全性是有效的，但仍存在不足之處.未來的工作主要分為以下三部分：

1)本文建立的WBS的SLIM模型尚有改進空間，在建模時對于液壓調節系統的所有子組件，只考慮了液壓的輸入和輸出，而沒考慮子組件造成液壓的損耗.因此，下一步將完善機輪剎車系統的形式化模型；

2)對于模型的安全性分析，目前只考慮了定性屬性，接下來會在模型中增加概率性屬性[26]，進一步對WBS進行性能分析；

3)本文研究是從系統的架構層出發，未來將考慮系統的需求層面，證明WBS需求的一致性和完備性.