| 自动飞行模式转换逻辑的形式化建模与验证 |
| |
| 引用本文： | 李俊安,胡军,王立松,黄志球,蔡鑫.自动飞行模式转换逻辑的形式化建模与验证[J].南京航空航天大学学报,2023,55(5):768-779. |
| |
| 作者姓名： | 李俊安 胡军 王立松 黄志球 蔡鑫 |
| |
| 作者单位： | 1.南京航空航天大学计算机科学与技术学院, 南京 211106;2.软件新技术与产业化协同创新中心, 南京 210007 |
| |
| 基金项目： | 国家自然科学基金（U2241216）。 |
| |
| 摘 要： | 自动飞行控制系统（Automatic flight control system,AFCS）是现代飞机中重要的安全关键系统之一，飞行引导控制系统（Flight guidance control system,FGCS）是其重要的组成部分。FGCS中的飞行模式有数十种，模式转换逻辑十分复杂，在各个模式间转换时易出现模式混淆等问题，难以对其安全性和正确性进行验证。而利用计算机科学中的形式化方法，通过对安全关键系统进行形式化建模和验证，可以提高系统的正确性和安全性。本文以典型FGCS中的自动飞行模式转换逻辑作为研究对象，采用自主研制的软件工具ART(Avionics requirement tool)对其进行形式化建模与验证，并与Matlab/Simulink中的Design Verifier工具进行了验证能力和效率的对比分析。实例研究结果表明，采用形式化方法对FGCS的自动飞行模式转换逻辑进行建模、验证可行，所研制的软件平台具有更完善的验证能力和更好的验证效率。
|
| 关 键 词： | 计算机软件与理论 飞行制导控制系统 基于模型的安全性分析 模型检测 安全关键系统 |
| 收稿时间： | 2023/3/14 0:00:00 |
| 修稿时间： | 2023/5/11 0:00:00 |
Formal Modeling and Verification of Automatic Flight Mode Transition Logic |
| |
| Li Junan,Hu Jun,Wang Lisong,Huang Zhiqiu,Cai Xin.Formal Modeling and Verification of Automatic Flight Mode Transition Logic[J].Journal of Nanjing University of Aeronautics & Astronautics,2023,55(5):768-779. |
| |
| Authors: | Li Junan Hu Jun Wang Lisong Huang Zhiqiu Cai Xin |
| |
| Abstract: | |
| |
| Keywords: | computer software and theory flight guidance control system model-based safety analysis model checking safety-critical system |
|
| 点击此处可从《南京航空航天大学学报》浏览原始摘要信息 |
| 点击此处可从《南京航空航天大学学报》下载免费的PDF全文 |
