形式化建模（一）

作者 |鄭寒月上?？匕部尚跑浖?chuàng)新研究院工程師

版塊 |鑒源論壇 · 觀模

01什么是建模

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

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

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

下面給出一個狀態(tài)機建模的實例。

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

表1打滑補償

圖1狀態(tài)機建模結(jié)果

02什么是形式化建模

形式化方法（Formal Method）是一種基于數(shù)學(xué)基礎(chǔ)，經(jīng)過嚴(yán)格的數(shù)學(xué)證明的分析技術(shù)的應(yīng)用方法，常用于軟件和硬件系統(tǒng)的描述、開發(fā)和驗證過程中。形式化建模則將形式化方法應(yīng)用于建模過程中，它以無歧義的形式化規(guī)格說明語言為基礎(chǔ)，使用精確定義的形式語言進行系統(tǒng)功能的描述，利用一些已知特性的數(shù)學(xué)抽象來為目標(biāo)軟件系統(tǒng)的狀態(tài)特征和行為特征構(gòu)造模型，從而完成形式化建模過程。形式化模型應(yīng)介于程序設(shè)計語言和高層需求之間，具有精確、無歧義的特點，但并不呈現(xiàn)過多細(xì)節(jié)。

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

03航空發(fā)動機控制軟件建模實例

因為安全攸關(guān)領(lǐng)域嵌入式控制軟件研制具有領(lǐng)域?qū)＜覅⑴c度高、功能安全性要求高、規(guī)范與標(biāo)準(zhǔn)約束嚴(yán)格等特點，所以為符合研制要求，保證系統(tǒng)安全，形式化建模廣泛運用于航空航天、軌道交通等安全攸關(guān)領(lǐng)域。

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

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

通過系統(tǒng)調(diào)研，可以提取出航空發(fā)動機控制系統(tǒng)的如下特征：

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

（2）控制軟件的輸出為經(jīng)過復(fù)雜算法計算之后的數(shù)值結(jié)果，通過計算的方式實現(xiàn)控制行為。

（3）控制軟件的基本時間單元為周期。因為實時性的要求，控制算法需要在給定周期內(nèi)完成相應(yīng)的算法計算。整個系統(tǒng)中有兩個周期概念，按照執(zhí)行功能的實時性分為了大閉環(huán)周期和小閉環(huán)周期，大閉環(huán)的周期值是小閉環(huán)周期的固定倍數(shù)。

（4）控制軟件的核心是控制規(guī)律，控制軟件在特定的狀態(tài)下有其固有的控制規(guī)律。

（5）控制軟件的主導(dǎo)因素是其當(dāng)前所處的狀態(tài)。系統(tǒng)在整個生命周期內(nèi)在不同的狀態(tài)下執(zhí)行不同的控制算法，具體調(diào)用的控制算法種類及其執(zhí)行順序由當(dāng)前時刻其所處的狀態(tài)決定。特別地，在每個周期的計算任務(wù)完成后，系統(tǒng)會檢測是否滿足狀態(tài)遷移條件。當(dāng)且僅當(dāng)滿足遷移條件時，系統(tǒng)的狀態(tài)會發(fā)生遷移。

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

由于傳統(tǒng)的形式化語言學(xué)習(xí)成本高、難以用于描述上述航空發(fā)動機控制系統(tǒng)特征等原因，本例采用了航空領(lǐng)域適用的具有以計算任務(wù)為核心、以模式為基礎(chǔ)、以周期為基本時間單元、按重要程度劃分層級等特征的形式化建模語言AEDL進行模型構(gòu)建。

遵循AEDL語義，使用AEDL語法構(gòu)建的航空發(fā)動機控制系統(tǒng)模型具有模式流、計算任務(wù)、數(shù)據(jù)字典等三個部分，分別對系統(tǒng)狀態(tài)轉(zhuǎn)換、系統(tǒng)計算執(zhí)行和系統(tǒng)變量進行了精確描述。

通過狀態(tài)轉(zhuǎn)換部分模型，可以對航空發(fā)動機的行為模式進行抽象，如圖2所示。

圖2航空發(fā)動機控制系統(tǒng)狀態(tài)轉(zhuǎn)換

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

（1）當(dāng)前航空發(fā)動機系統(tǒng)具有10個合法模式；

（2）模式轉(zhuǎn)換需滿足相應(yīng)的條件；

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

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

......

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

圖3初始模式轉(zhuǎn)換

該形式化建模案例體現(xiàn)了航空發(fā)動機控制系統(tǒng)周期控制、具有模式狀態(tài)遷移、以計算任務(wù)為主等行為特征。基于形式化模型的分析驗證，我們將在后續(xù)文章中作更為深入和系統(tǒng)化的討論。

參考文獻(xiàn)：

[1] EN50128、DO-333等工業(yè)標(biāo)準(zhǔn).

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

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

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

[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.

審核編輯 黃昊宇