形式化建模（一）

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

版塊 |鑒源論壇 · 觀模

01什么是建模

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

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

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

下面給出一個(gè)狀態(tài)機(jī)建模的實(shí)例。

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

表1打滑補(bǔ)償

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

02什么是形式化建模

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

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

03航空發(fā)動(dòng)機(jī)控制軟件建模實(shí)例

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

接下來(lái)將以航空發(fā)動(dòng)機(jī)控制系統(tǒng)為例，介紹形式化建模在工程上的運(yùn)用。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

......

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

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

該形式化建模案例體現(xiàn)了航空發(fā)動(dòng)機(jī)控制系統(tǒng)周期控制、具有模式狀態(tài)遷移、以計(jì)算任務(wù)為主等行為特征?；谛问交Ｐ偷姆治鲵?yàn)證，我們將在后續(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] 蔡喁, 形式化方法在民機(jī)機(jī)載軟件中的應(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.

審核編輯 黃昊宇