面向国产机载操作系统的IMA软件代码生成方法
An Approach for IMA Software Code Generation on Domestic Airborne Operating System
凌仕翔 1杨志斌 1郭鹏 2周勇1
作者信息
- 1. 南京航空航天大学,江苏 南京 211000;高安全系统的软件开发与验证技术工信部重点实验室,江苏 南京 211000
- 2. 航空工业西安航空计算技术研究所,陕西 西安 710000
- 折叠
摘要
随着航空电子系统复杂化的发展趋势及自主可控的要求,对这类复杂系统建模后如何自动生成面向国产机载操作系统的软件代码并验证模型/代码语义一致性具有重要研究意义.文章提出面向国产机载操作系统的航空电子软件代码自动生成方法.首先,使用AADL对综合化航空电子系统进行建模,设计AADL模型到源代码的转换规则,自动生成面向国产机载操作系统的平台相关代码及配置文件;其次,通过AGREE Annex和BLESS Annex契约对AADL模型进行形式化验证,并提出契约到C语言验证代码的转换规则,将验证代码与模型生成的源代码进行结合,部署在国产机载操作系统上进行仿真执行;最后,基于AADL开源建模环境OSATE设计并实现了代码自动生成工具,实验结果验证了方法和工具的有效性.
Abstract
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 air-borne 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 air-borne operating system.Firstly,AADL is used to model the integrated avionics system,and the transforma-tion 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 genera-ted by the model,and deploy it on the domestic airborne operating system for simulation execution.Final-ly,an automatic code generation tool is designed and implemented based on the open source modeling en-vironment OSATE,and the experimental results verify the effectiveness of the proposed method and tool.
关键词
综合模块化航空电子系统/国产机载操作系统/AADL/代码生成/模型/代码语义一致性Key words
integrated avionic systems/domestic airborne operating system/architecture analysis and de-sign language/code generation/model/code semantic consistency引用本文复制引用
基金项目
国家自然科学基金项目(62072233)
航空科学基金(201919052002)
出版年
2024
NETL
NSTL
万方数据