检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
作 者:凌仕翔 杨志斌[1,2] 郭鹏 周勇 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)
机构地区:[1]南京航空航天大学,江苏南京211000 [2]高安全系统的软件开发与验证技术工信部重点实验室,江苏南京211000 [3]航空工业西安航空计算技术研究所,陕西西安710000
出 处:《航空计算技术》2024年第4期84-88,93,共6页Aeronautical Computing Technique
基 金:国家自然科学基金项目(62072233);航空科学基金项目资助(201919052002)。
摘 要:随着航空电子系统复杂化的发展趋势及自主可控的要求,对这类复杂系统建模后如何自动生成面向国产机载操作系统的软件代码并验证模型/代码语义一致性具有重要研究意义。文章提出面向国产机载操作系统的航空电子软件代码自动生成方法。首先,使用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.
关 键 词:综合模块化航空电子系统 国产机载操作系统 AADL 代码生成 模型/代码语义一致性
分 类 号:TP311[自动化与计算机技术—计算机软件与理论]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:52.14.137.94