孟開元　王瑾　彭寒　曹慶年

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

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

中圖分類號：v227+.4;? 文獻標(biāo)識碼：A

文章編號：1009-3044（2022）07-0100-02

1 概述

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

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

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

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

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

3.1 建模的具體過程

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

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

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

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

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

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

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

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

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

3.2 結(jié)果分析

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

4 總結(jié)

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

參考文獻：

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

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

[3] 彭寒，張曉麗，劉洲洲，等.基于Event-B的軟件工程形式化方法綜述[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é)報（自然科學(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] 李夢君.基于Event-B和Rodin開展形式化軟件工程教學(xué)[J].計算機工程與科學(xué)，2016，38（S1）：143-145.

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

收稿日期：2021-09-28

作者簡介：孟開元（1968—），男，江蘇海安人，工學(xué)碩士，副教授，研究方向為嵌入式自動化;王瑾（1995—）女，陜西西安人，碩士。