面向国产机载操作系统的IMA软件代码生成方法

An Approach for IMA Software Code Generation on Domestic Airborne Operating System

随着航空电子系统复杂化的发展趋势及自主可控的要求,对这类复杂系统建模后如何自动生成面向国产机载操作系统的软件代码并验证模型/代码语义一致性具有重要研究意义。文章提出面向国产机载操作系统的航空电子软件代码自动生成方法。首先,使用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.