基于EVENT-B的飞机起落架控制系统形式化建模

孟开元　王瑾　彭寒　曹庆年

摘要：飞机起落架控制系统作为飞机的一个极其重要的部分，在飞机着陆、滑跑、起飞过程中起着非常重要的作用，该部分系统性能的好坏将直接影响整个飞机的安全性。飞机起落架系统作为一个极其复杂的系统，如果使用传统的建模语言对其进行建模，可能会使整个建模过程变得特别复杂，所以这里选择形式化语言Event-B和可视化插件IUML-B对其建模，这对飞机起落架控制系统的开发与研究有着重要的意义。

关键词：起落架;形式化建模;EVENT-B;IUML-B;精化

中图分类号：v227+.4;  文献标识码：A

文章编号：1009-3044（2022）07-0100-02

1 概述

随着飞机行业的进步与发展，对飞机安全性的要求也越来越高，起落架控制系统开发是研究飞机安全性的重要环节，它是飞机在地面着陆停放、起飞滑跑时用于支撑飞机重力并承受相应载荷的装置，它能够消耗和吸收飞机在着陆时的撞击能量，并且它在飞机机体和机轮刹车系统的之间起着桥梁作用，故其设计性能的优劣是直接影响着飞机起飞和着陆的关键因素[1]。Event-B 语言是法国科学家 Abrial在B语言、Action 系统基础上提出的一种基于模型的形式化建模语言[2]，已广泛运用于航空航天领域。近几年不少机构也基于Event-B语言做了很多研究，但这些研究都没有涉及起落架控制系统方面，所以本文将使用 Event-B语言对飞机起落架控制系统进行建模[3]。但使用这一种方法是不够的，因为Event-B语言虽然解决了一些问题，但是对于建模可视化配置的需求还有些欠缺，并且Event-B 设计模式的实例化需要手工编写大量的模型代码，最终导致研究工作的效率大大降低[4]。因此，本文结合Event-B建模语言和可视化插件IUML-B来对飞机起落架控制系统形式化建模，通过使用这两种建模工具，建模的效率将会显著提高[5]。

2 起落架控制系统原理分析

起落架控制系统包括手柄、起落架、门三个基础设备以及四个特定电动阀、一个通用电动阀、模拟开关、信号灯等辅助设备。通用电动阀为整个回路提供液压，它控制整个系统的运行，同时受到模拟开关的限制，通用电动阀只有在模拟开关闭合后才可以打开。特定电动阀直接控制基础设备的运行，同时受到通用电动阀的限制。信号灯的设计是为了便于驾驶员更直接地了解起落架的状态及故障情况[6]。起落架控制系统原理如图1所示。

图中P表示液压、D表示门、G表示起落架、T表示通用电动阀、O表示开门电动阀、C表示关门电动阀、E表示伸出齿轮电动阀、R表示收回起落架电动阀。

3 起落架控制系统建模设计

3.1 建模的具体过程

本次建模采用逐级精化的方式，将飞机起落架系统分为六层，首先建立起落架控制系统的抽象模型，确定起落架的所有可能的动作及状态，建立起落架状态机。

（1） 第一层精化是在抽象模型的基础上加入了门的模型，建立了门状态机，此时有两个状态机，起落架和门，该层的目的是同步门和起落架，使两者不再独立，它们之间的动作和状态都要受到对方的约束。

（2） 第二层精化则是在第一层的基础上添加了手柄模型，建立了手柄状态机，此时起落架、手柄、门三个之间就形成了一种相互制约关系。

（3） 第三层精化则是在第二层的基础上添加了特定电动阀模型，建立了四种特定电动阀状态机，分别是开门电动阀、关门电动阀、伸出起落架电动阀、收回起落架电动阀，特定电动阀状态机主要是约束了起落架和门这两种设备的动作和状态。

（4） 第四层精化则是在第三层的基础上添加了飞机的起飞和着陆模型，建立了飞机的起飞与着陆状态机，同样该状态机和其他所有状态机之间也有一种相互制约关系。

（5） 第五层精化添加了通用电动阀和模拟开关模型，建立了模拟开关状态机和通用电动阀状态机，通用电动阀状态机约束了特定电动阀状态机，反过来又被模拟开关状态机影响。

（6） 第六层精化主要是添加了信号灯状态机，信号灯状态机可以显示当前飞机运行的状态及故障情况。

接下来由下面的图2来为大家展示一下精化的含义，以及各状态机之间的制约关系。

上图展示了起落架状态机的发展历程，在图2上半部分的图片中我们可以看出，起落架有四种状态，六个事件，这六个事件都是关于起落架本身的，起落架在此时还是一个独立的设备，后来经过逐步精化，和其他的设备之间产生了相互制约的关系，它开始受到门还有手柄对它的影响，初始时起落架伸出，门关闭，手柄向下，如果此时手柄反转向上，起落架受制于手柄就会做出收回的动作，而此时门了解到起落架需要收回的意图，门的状态也会由关闭状态开始打开，其中可能牵扯了几十种状态转换关系，不同的激励造成的结果就不一样，所以在图2 的下半部分中可以看到十几种可能发生的事件。

3.2 结果分析

RODIN平台提供了一系列功能以支持使用Event-B进行以精化为基础的建模，其中的自动定理证明功能将建模和证明无缝地结合起来，为我们扫清了不少障碍[7]。下面图3是每一层定理证明的结果，每一层结果显示未证明的定理为0，证明每一级的建模正确。

4 总结

该文对飞机起落架控制系统形式化建模，从需求文档出发得到精化策略，通过一系列逐步精化的模型，最终完成了起落架控制系统的建模。结合 Event-B 语言和可视化插件 iUML-B，成功地完成了对飞机起落架 控制系统的建模，并使用仿真工具 ProB 仿真通过。随着实际生活中的飞机起落架控制系统要求更多杂，往往需要考虑系统的实时控制需求。例如门的状态 本文中就涉及了十种状态转换，但本文仅仅实现了这十种状态的相互转换，并没有具体研究十种状态转换间的时序关系。如果考虑到状态间的时序关系，就可将十种状态具体化。可想而知这是非常复杂的。因此，在今后的学习中，为了确保系统的完整性，将花费更多的精力和时间研究状态间的时序关系。

参考文献：

[1] 赵兴平，彭纲，常凯，等.飞机起落架舱门作动同步控制研究[J].机电工程技术，2021，50（9）：232-235.

[2] 陈志慧.基于Event-B的软件需求形式化建模技术的研究[D].成都：电子科技大学，2013.

[3] 彭寒，张晓丽，刘洲洲，等.基于Event-B的软件工程形式化方法综述[J].计算机系统应用，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].江苏科技大学学报（自然科学版），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开展形式化软件工程教学[J].计算机工程与科学，2016，38（S1）：143-145.

【通聯编辑：梁书】

收稿日期：2021-09-28

作者简介：孟开元（1968—），男，江苏海安人，工学硕士，副教授，研究方向为嵌入式自动化;王瑾（1995—）女，陕西西安人，硕士。