| 自动飞行模式转换逻辑的形式化建模与验证 |
| |
| 引用本文： | 李俊安,胡军,王立松,黄志球,蔡鑫. 自动飞行模式转换逻辑的形式化建模与验证[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-03-14 |
| 修稿时间： | 2023-05-11 |
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 |
|
| 点击此处可从《南京航空航天大学学报》浏览原始摘要信息 |
|
点击此处可从《南京航空航天大学学报》下载全文 |
|
