作者 |鄭寒月上?？匕部尚跑浖撔卵芯吭?a target="_blank">工程師

版塊 |鑒源論壇 · 觀模

01什么是建模

對系統進行建模是一個采用表格化、圖形化、公式化的方式，將系統的構成及其構成間的關系呈現給人們的一種技術方法，也就是將系統進行抽象化處理的過程。對系統的抽象可以從多個層面進行，即可以從多維度進行建模。在建模過程中，系統逐漸實現無歧義化的過程。

數據層面的建模通常在數據流的基礎上進行。數據流是一組有序、有起點和終點的數據序列。數據流圖（Data Flow Diagram）描述數據如何在軟件功能模塊之間“流動”，主要從功能之間的數據信息傳遞關系層面來刻畫系統，可對系統功能進行層次化的組合描述。其主要描述對象為：處理數據的功能（Process），數據資源的集合（Data Store）和數據的流動（Data Flow）。

另一種常用的建模方式是使用有限狀態機（Finite-state Machine）進行建模。狀態機模型中包含四個基本要素，分別為現態、條件、動作和次態。現態指當前周期所處的狀態。條件指當某個狀態滿足一定條件時，會觸發一次動作，或執行一次遷移。動作執行完畢后，可以遷移到新的狀態，或者保持原狀態。次態指基于當前所處狀態，條件滿足后需要遷往的新狀態。若基于狀態機模型進行模擬仿真，需首先通過輸入端口確定現態，執行一次動作后判斷現態的所有遷移條件是否滿足，若滿足遷移條件則發生跳轉，若不滿足則仍保持現態，同時傳出輸出變量；若滿足遷移條件則發生跳轉，并執行一次動作。

下面給出一個狀態機建模的實例。

在軌道交通領域，由于慣性，每次停車可能發生車輪與軌道的“打滑”，使得軟件記錄的車輪運行圈數和實際運行圈數不一致，累計以后容易導致錯誤計算。為確保安全，需要監控打滑的距離等數值，計算一個補償數值，使得車輪實際運行圈數與計算值一致。對于如表1所示的描述進行狀態機建模，可知空轉補償狀態有COASTING、BRAKING、SLIDING、SKIDDING等四個狀態，關注列車車輪打滑監控模塊，抽取出狀態和遷移條件進行狀態機建模。狀態機建模結果如圖1所示，其中COASTING、BRAKING、SLIDING、SKIDDING為狀態，箭頭表示遷移，遷移條件表示在遷移箭頭上，數字代表遷移條件數量。

表1打滑補償

圖1狀態機建模結果

02什么是形式化建模

形式化方法（Formal Method）是一種基于數學基礎，經過嚴格的數學證明的分析技術的應用方法，常用于軟件和硬件系統的描述、開發和驗證過程中。形式化建模則將形式化方法應用于建模過程中，它以無歧義的形式化規格說明語言為基礎，使用精確定義的形式語言進行系統功能的描述，利用一些已知特性的數學抽象來為目標軟件系統的狀態特征和行為特征構造模型，從而完成形式化建模過程。形式化模型應介于程序設計語言和高層需求之間，具有精確、無歧義的特點，但并不呈現過多細節。

一些經典的形式化語言，如Z語言、B語言、Event-B語言、VDM等均具有各自的形式語義，使用形式化語言遵循建模規范得到的形式化模型可以對系統進行精確描述，便于進行后續的形式化分析和驗證。

03航空發動機控制軟件建模實例

因為安全攸關領域嵌入式控制軟件研制具有領域專家參與度高、功能安全性要求高、規范與標準約束嚴格等特點，所以為符合研制要求，保證系統安全，形式化建模廣泛運用于航空航天、軌道交通等安全攸關領域。

接下來將以航空發動機控制系統為例，介紹形式化建模在工程上的運用。

航空發動機控制軟件是實時嵌入式軟件，運行于電子控制器平臺（EEC）中實現發動機的運行控制，主要功能是按照飛機的指令實現發動機的啟動、停車、推力控制、限制保護、作動部件控制、故障診斷及處理等。

通過系統調研，可以提取出航空發動機控制系統的如下特征：

（1）控制軟件輸入為各傳感器變量。

（2）控制軟件的輸出為經過復雜算法計算之后的數值結果，通過計算的方式實現控制行為。

（3）控制軟件的基本時間單元為周期。因為實時性的要求，控制算法需要在給定周期內完成相應的算法計算。整個系統中有兩個周期概念，按照執行功能的實時性分為了大閉環周期和小閉環周期，大閉環的周期值是小閉環周期的固定倍數。

（4）控制軟件的核心是控制規律，控制軟件在特定的狀態下有其固有的控制規律。

（5）控制軟件的主導因素是其當前所處的狀態。系統在整個生命周期內在不同的狀態下執行不同的控制算法，具體調用的控制算法種類及其執行順序由當前時刻其所處的狀態決定。特別地，在每個周期的計算任務完成后，系統會檢測是否滿足狀態遷移條件。當且僅當滿足遷移條件時，系統的狀態會發生遷移。

因此，在建模過程中可以將航空發動機控制軟件視為一個以周期為基本時間單元驅動的具有多個不同發動機狀態的控制系統。在發動機處于每個特定狀態時，它可以根據設定的時間周期，完成模式內具體的采樣、計算任務和控制行為，并判斷給定的條件，完成可能的狀態切換或繼續處于當前狀態的判定。

由于傳統的形式化語言學習成本高、難以用于描述上述航空發動機控制系統特征等原因，本例采用了航空領域適用的具有以計算任務為核心、以模式為基礎、以周期為基本時間單元、按重要程度劃分層級等特征的形式化建模語言AEDL進行模型構建。

遵循AEDL語義，使用AEDL語法構建的航空發動機控制系統模型具有模式流、計算任務、數據字典等三個部分，分別對系統狀態轉換、系統計算執行和系統變量進行了精確描述。

通過狀態轉換部分模型，可以對航空發動機的行為模式進行抽象，如圖2所示。

圖2航空發動機控制系統狀態轉換

頂層的狀態代表航空發動機控制系統可能處于的狀態，箭頭的方向從現態指向可進行遷移的次態，遷移條件對遷移是否合法進行了限制。狀態轉換圖可以描述航空發動機控制系統的整體行為，通過相應的狀態轉換圖進行研究，可以理解系統行為，分析出系統的部分特征。如：

（1）當前航空發動機系統具有10個合法模式；

（2）模式轉換需滿足相應的條件；

（3）所有的模式均有可以到達的途徑；

（4）模式間的遷移條件可能由多個表達式組合而成；

......

具有經驗的工程師可以根據狀態模型快速判斷出系統狀態是否存在問題。比如，如圖3所示的初始模式轉換，飛行控制人員可能根據其專業知識，認定“初始模式”不應該以當前條件直接轉換到“慢車以上模式”。任何一個模式，都不應該同時滿足向兩個及以上模式轉換的條件，否則意味著系統可能會出現不確定性，發生模式的隨意轉換。

圖3初始模式轉換

該形式化建模案例體現了航空發動機控制系統周期控制、具有模式狀態遷移、以計算任務為主等行為特征?；谛问交Ｐ偷姆治鲵炞C，我們將在后續文章中作更為深入和系統化的討論。

參考文獻：

[1] EN50128、DO-333等工業標準.

[2] 王政, 嵌入式周期控制系統的建模與分析, 2012, 華東師范大學.

[3] Spivey, J.M., The Z notation: a reference manual. International, 1990. 15(2-3): p. 253-255.

[4] 蔡喁, 形式化方法在民機機載軟件中的應用及適航考慮.

[5]Abrial, J.R., Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. 2010: DBLP. 428-430.

[6]Miao, W. and S. Liu, A Formal Engineering Framework for Service-Based Software Modeling. IEEE Transactions on Services Computing, 2013. 6(4): p. 536-550.

審核編輯 黃昊宇