基于EVENT-B的飛機(jī)起落架控制系統(tǒng)形式化建模

孟開元　王瑾　彭寒　曹慶年

摘要：飛機(jī)起落架控制系統(tǒng)作為飛機(jī)的一個(gè)極其重要的部分，在飛機(jī)著陸、滑跑、起飛過程中起著非常重要的作用，該部分系統(tǒng)性能的好壞將直接影響整個(gè)飛機(jī)的安全性。飛機(jī)起落架系統(tǒng)作為一個(gè)極其復(fù)雜的系統(tǒng)，如果使用傳統(tǒng)的建模語(yǔ)言對(duì)其進(jìn)行建模，可能會(huì)使整個(gè)建模過程變得特別復(fù)雜，所以這里選擇形式化語(yǔ)言Event-B和可視化插件IUML-B對(duì)其建模，這對(duì)飛機(jī)起落架控制系統(tǒng)的開發(fā)與研究有著重要的意義。

關(guān)鍵詞：起落架;形式化建模;EVENT-B;IUML-B;精化

中圖分類號(hào)：v227+.4;? 文獻(xiàn)標(biāo)識(shí)碼：A

文章編號(hào)：1009-3044（2022）07-0100-02

1 概述

隨著飛機(jī)行業(yè)的進(jìn)步與發(fā)展，對(duì)飛機(jī)安全性的要求也越來越高，起落架控制系統(tǒng)開發(fā)是研究飛機(jī)安全性的重要環(huán)節(jié)，它是飛機(jī)在地面著陸停放、起飛滑跑時(shí)用于支撐飛機(jī)重力并承受相應(yīng)載荷的裝置，它能夠消耗和吸收飛機(jī)在著陸時(shí)的撞擊能量，并且它在飛機(jī)機(jī)體和機(jī)輪剎車系統(tǒng)的之間起著橋梁作用，故其設(shè)計(jì)性能的優(yōu)劣是直接影響著飛機(jī)起飛和著陸的關(guān)鍵因素[1]。Event-B 語(yǔ)言是法國(guó)科學(xué)家 Abrial在B語(yǔ)言、Action 系統(tǒng)基礎(chǔ)上提出的一種基于模型的形式化建模語(yǔ)言[2]，已廣泛運(yùn)用于航空航天領(lǐng)域。近幾年不少機(jī)構(gòu)也基于Event-B語(yǔ)言做了很多研究，但這些研究都沒有涉及起落架控制系統(tǒng)方面，所以本文將使用 Event-B語(yǔ)言對(duì)飛機(jī)起落架控制系統(tǒng)進(jìn)行建模[3]。但使用這一種方法是不夠的，因?yàn)镋vent-B語(yǔ)言雖然解決了一些問題，但是對(duì)于建?？梢暬渲玫男枨筮€有些欠缺，并且Event-B 設(shè)計(jì)模式的實(shí)例化需要手工編寫大量的模型代碼，最終導(dǎo)致研究工作的效率大大降低[4]。因此，本文結(jié)合Event-B建模語(yǔ)言和可視化插件IUML-B來對(duì)飛機(jī)起落架控制系統(tǒng)形式化建模，通過使用這兩種建模工具，建模的效率將會(huì)顯著提高[5]。

2 起落架控制系統(tǒng)原理分析

起落架控制系統(tǒng)包括手柄、起落架、門三個(gè)基礎(chǔ)設(shè)備以及四個(gè)特定電動(dòng)閥、一個(gè)通用電動(dòng)閥、模擬開關(guān)、信號(hào)燈等輔助設(shè)備。通用電動(dòng)閥為整個(gè)回路提供液壓，它控制整個(gè)系統(tǒng)的運(yùn)行，同時(shí)受到模擬開關(guān)的限制，通用電動(dòng)閥只有在模擬開關(guān)閉合后才可以打開。特定電動(dòng)閥直接控制基礎(chǔ)設(shè)備的運(yùn)行，同時(shí)受到通用電動(dòng)閥的限制。信號(hào)燈的設(shè)計(jì)是為了便于駕駛員更直接地了解起落架的狀態(tài)及故障情況[6]。起落架控制系統(tǒng)原理如圖1所示。

圖中P表示液壓、D表示門、G表示起落架、T表示通用電動(dòng)閥、O表示開門電動(dòng)閥、C表示關(guān)門電動(dòng)閥、E表示伸出齒輪電動(dòng)閥、R表示收回起落架電動(dòng)閥。

3 起落架控制系統(tǒng)建模設(shè)計(jì)

3.1 建模的具體過程

本次建模采用逐級(jí)精化的方式，將飛機(jī)起落架系統(tǒng)分為六層，首先建立起落架控制系統(tǒng)的抽象模型，確定起落架的所有可能的動(dòng)作及狀態(tài)，建立起落架狀態(tài)機(jī)。

（1） 第一層精化是在抽象模型的基礎(chǔ)上加入了門的模型，建立了門狀態(tài)機(jī)，此時(shí)有兩個(gè)狀態(tài)機(jī)，起落架和門，該層的目的是同步門和起落架，使兩者不再獨(dú)立，它們之間的動(dòng)作和狀態(tài)都要受到對(duì)方的約束。

（2） 第二層精化則是在第一層的基礎(chǔ)上添加了手柄模型，建立了手柄狀態(tài)機(jī)，此時(shí)起落架、手柄、門三個(gè)之間就形成了一種相互制約關(guān)系。

（3） 第三層精化則是在第二層的基礎(chǔ)上添加了特定電動(dòng)閥模型，建立了四種特定電動(dòng)閥狀態(tài)機(jī)，分別是開門電動(dòng)閥、關(guān)門電動(dòng)閥、伸出起落架電動(dòng)閥、收回起落架電動(dòng)閥，特定電動(dòng)閥狀態(tài)機(jī)主要是約束了起落架和門這兩種設(shè)備的動(dòng)作和狀態(tài)。

（4） 第四層精化則是在第三層的基礎(chǔ)上添加了飛機(jī)的起飛和著陸模型，建立了飛機(jī)的起飛與著陸狀態(tài)機(jī)，同樣該狀態(tài)機(jī)和其他所有狀態(tài)機(jī)之間也有一種相互制約關(guān)系。

（5） 第五層精化添加了通用電動(dòng)閥和模擬開關(guān)模型，建立了模擬開關(guān)狀態(tài)機(jī)和通用電動(dòng)閥狀態(tài)機(jī)，通用電動(dòng)閥狀態(tài)機(jī)約束了特定電動(dòng)閥狀態(tài)機(jī)，反過來又被模擬開關(guān)狀態(tài)機(jī)影響。

（6） 第六層精化主要是添加了信號(hào)燈狀態(tài)機(jī)，信號(hào)燈狀態(tài)機(jī)可以顯示當(dāng)前飛機(jī)運(yùn)行的狀態(tài)及故障情況。

接下來由下面的圖2來為大家展示一下精化的含義，以及各狀態(tài)機(jī)之間的制約關(guān)系。

上圖展示了起落架狀態(tài)機(jī)的發(fā)展歷程，在圖2上半部分的圖片中我們可以看出，起落架有四種狀態(tài)，六個(gè)事件，這六個(gè)事件都是關(guān)于起落架本身的，起落架在此時(shí)還是一個(gè)獨(dú)立的設(shè)備，后來經(jīng)過逐步精化，和其他的設(shè)備之間產(chǎn)生了相互制約的關(guān)系，它開始受到門還有手柄對(duì)它的影響，初始時(shí)起落架伸出，門關(guān)閉，手柄向下，如果此時(shí)手柄反轉(zhuǎn)向上，起落架受制于手柄就會(huì)做出收回的動(dòng)作，而此時(shí)門了解到起落架需要收回的意圖，門的狀態(tài)也會(huì)由關(guān)閉狀態(tài)開始打開，其中可能牽扯了幾十種狀態(tài)轉(zhuǎn)換關(guān)系，不同的激勵(lì)造成的結(jié)果就不一樣，所以在圖2 的下半部分中可以看到十幾種可能發(fā)生的事件。

3.2 結(jié)果分析

RODIN平臺(tái)提供了一系列功能以支持使用Event-B進(jìn)行以精化為基礎(chǔ)的建模，其中的自動(dòng)定理證明功能將建模和證明無縫地結(jié)合起來，為我們掃清了不少障礙[7]。下面圖3是每一層定理證明的結(jié)果，每一層結(jié)果顯示未證明的定理為0，證明每一級(jí)的建模正確。

4 總結(jié)

該文對(duì)飛機(jī)起落架控制系統(tǒng)形式化建模，從需求文檔出發(fā)得到精化策略，通過一系列逐步精化的模型，最終完成了起落架控制系統(tǒng)的建模。結(jié)合 Event-B 語(yǔ)言和可視化插件 iUML-B，成功地完成了對(duì)飛機(jī)起落架 控制系統(tǒng)的建模，并使用仿真工具 ProB 仿真通過。隨著實(shí)際生活中的飛機(jī)起落架控制系統(tǒng)要求更多雜，往往需要考慮系統(tǒng)的實(shí)時(shí)控制需求。例如門的狀態(tài) 本文中就涉及了十種狀態(tài)轉(zhuǎn)換，但本文僅僅實(shí)現(xiàn)了這十種狀態(tài)的相互轉(zhuǎn)換，并沒有具體研究十種狀態(tài)轉(zhuǎn)換間的時(shí)序關(guān)系。如果考慮到狀態(tài)間的時(shí)序關(guān)系，就可將十種狀態(tài)具體化?？上攵@是非常復(fù)雜的。因此，在今后的學(xué)習(xí)中，為了確保系統(tǒng)的完整性，將花費(fèi)更多的精力和時(shí)間研究狀態(tài)間的時(shí)序關(guān)系。

參考文獻(xiàn)：

[1] 趙興平，彭綱，常凱，等.飛機(jī)起落架艙門作動(dòng)同步控制研究[J].機(jī)電工程技術(shù)，2021，50（9）：232-235.

[2] 陳志慧.基于Event-B的軟件需求形式化建模技術(shù)的研究[D].成都：電子科技大學(xué)，2013.

[3] 彭寒，張曉麗，劉洲洲，等.基于Event-B的軟件工程形式化方法綜述[J].計(jì)算機(jī)系統(tǒng)應(yīng)用，2021，30（9）：12-23.

[4] Mammar A，Laleau R.Modeling a landing gear system in Event-B[J].International Journal on Software Tools for Technology Transfer，2017，19（2）：167-186.

[5] 夏志龍，高尚.基于Event-B形式化分析UML模型一致性[J].江蘇科技大學(xué)學(xué)報(bào)（自然科學(xué)版），2017，31（3）：327-332.

[6] Su W，Abrial J R.Aircraft landing gear system：approaches with Event-B to the modeling of an industrial system[J].International Journal on Software Tools for Technology Transfer，2017，19（2）：141-166.

[7] 李夢(mèng)君.基于Event-B和Rodin開展形式化軟件工程教學(xué)[J].計(jì)算機(jī)工程與科學(xué)，2016，38（S1）：143-145.

【通聯(lián)編輯：梁書】

收稿日期：2021-09-28

作者簡(jiǎn)介：孟開元（1968—），男，江蘇海安人，工學(xué)碩士，副教授，研究方向?yàn)榍度胧阶詣?dòng)化;王瑾（1995—）女，陜西西安人，碩士。