南京航空航天大学学报

作者：李俊安，胡军，王立松，黄志球，蔡鑫

单位：南京航空航天大学计算机科学与技术学院；,南京航空航天大学计算机科学与技术学院;软件新技术与产业化协同创新中心；,南京航空航天大学计算机科学与技术学院;软件新技术与产业化协同创新中心；,南京航空航天大学计算机科学与技术学院；,南京航空航天大学计算机科学与技术学院；

关键词：计算机软件与理论;飞行制导控制系统;基于模型的安全性分析;模型检测;安全关键系统

基金：国家自然科学基金（U2241216）。

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

来源：2023年第5期

《南京航空航天大学学报》期刊编辑部

查看南京航空航天大学学报杂志2023年第5期