自动飞行模式转换逻辑的形式化建模与验证

Formal Modeling and Verification of Automatic Flight Mode Transition Logic

自动飞行控制系统(Automatic flight control system,AFCS)是现代飞机中重要的安全关键系统之一,飞行引导控制系统(Flight guidance control system,FGCS)是其重要的组成部分。FGCS中的飞行模式有数十种,模式转换逻辑十分复杂,在各个模式间转换时易出现模式混淆等问题,难以对其安全性和正确性进行验证。而利用计算机科学中的形式化方法,通过对安全关键系统进行形式化建模和验证,可以提高系统的正确性和安全性。本文以典型FGCS中的自动飞行模式转换逻辑作为研究对象,采用自主研制的软件工具ART(Avionics requirement tool)对其进行形式化建模与验证,并与Matlab/Simulink中的Design Verifier工具进行了验证能力和效率的对比分析。实例研究结果表明,采用形式化方法对FGCS的自动飞行模式转换逻辑进行建模、验证可行,所研制的软件平台具有更完善的验证能力和更好的验证效率。

Automatic flight control system(AFCS)is one of the most important safety‑critical systems in modern aircraft,and flight guidance control system(FGCS)is an important part of it.There are dozens of flight modes in FGCS,and its mode conversion logic is very complex,which is prone to pattern confusion and other problems in the conversion of various modes,making it difficult to verify their safety and correctness.However,formal modeling and verification of safety‑critical systems can improve the correctness and safety of the system by using formal methods in computer science.This paper takes the automatic flight mode conversion logic of typical FGCS as the research object,uses the software tool ART(Avionics requirement tool)independently developed by the author team to carry out formal modeling and verification,and compares the verification ability and efficiency with the Design Verifier tool in Matlab/Simulink.The case study results show that it is feasible to model and verify the automatic flight mode conversion logic of FGCS using formal methods.Meanwhile,our software platform has more complete verification capability and better verification efficiency.