摘要
随着航空电子系统复杂化的发展趋势及自主可控的要求,对这类复杂系统建模后如何自动生成面向国产机载操作系统的软件代码并验证模型/代码语义一致性具有重要研究意义。文章提出面向国产机载操作系统的航空电子软件代码自动生成方法。首先,使用AADL对综合化航空电子系统进行建模,设计AADL模型到源代码的转换规则,自动生成面向国产机载操作系统的平台相关代码及配置文件;其次,通过AGREE Annex和BLESS Annex契约对AADL模型进行形式化验证,并提出契约到C语言验证代码的转换规则,将验证代码与模型生成的源代码进行结合,部署在国产机载操作系统上进行仿真执行;最后,基于AADL开源建模环境OSATE设计并实现了代码自动生成工具,实验结果验证了方法和工具的有效性。
With the development trend of complex avionics system and the requirement of autonomous control,it is of great significance to study how to automatically generate software code for domestic airborne operating system and verify the semantic consistency of model/code after modeling such complex systems.This paper proposes an automatic generation method of avionics software code for domestic airborne operating system.Firstly,AADL is used to model the integrated avionics system,and the transformation rules from AADL model to source code are designed to automatically generate platform-related code and configuration files for domestic airborne operating system.Secondly,the AGREE Annex and BLESS Annex contracts are used to formally verify the AADL model,and the transformation rules from contracts to C language verification code are proposed to combine the verification code with the source code generated by the model,and deploy it on the domestic airborne operating system for simulation execution.Finally,an automatic code generation tool is designed and implemented based on the open source modeling environment OSATE,and the experimental results verify the effectiveness of the proposed method and tool.
作者
凌仕翔
杨志斌
郭鹏
周勇
LING Shi-xiang;YANG Zhi-bin;GUO Peng;ZHOU Yong(Nanjing University of Aeronautics and Astronautics,Nanjing 211000,China;Key Laboratory of Safety-critical Software,Ministry of Industry and Information Technology,Nanjing 211000,China;Xi'an Aeronautics Computing Technique Research Institute,AVIC,Xi'an 710000,China)
出处
《航空计算技术》
2024年第4期84-88,93,共6页
Aeronautical Computing Technique
基金
国家自然科学基金项目(62072233)
航空科学基金项目资助(201919052002)。
关键词
综合模块化航空电子系统
国产机载操作系统
AADL
代码生成
模型/代码语义一致性
integrated avionic systems
domestic airborne operating system
architecture analysis and design language
code generation
model/code semantic consistency
