系统工程与电子技术

作者：刘嘉琛, 董磊, 赵长啸, 陈泓兵

单位：1. 中国民航大学安全科学与工程学院, 天津 300300；2. 中国民航大学民航航空器适航审定技术重点实验室, 天津 300300；3. 天津市民用航空器适航与维修重点实验室, 天津 300300

关键词：分布式综合模块化航空电子,动态重构,架构分析与设计语言,形式化方法,仿真验证

基金：国家自然科学基金-民航联合基金(U1933106);航空科学基金(20185167017);中央高校基本科研业务费(3122019167)

针对可重构分布式综合模块化航空电子(distributed integrated modular avionics, DIMA)系统在设计初期缺少仿真与验证手段的问题, 首先分析了可重构DIMA软件体系的架构特征以及支持动态重构的层次化通用系统管理(generic system management, GSM)的组件功能划分。然后, 使用架构分析与设计语言(architecture analysis and design language, AADL)及其相关附件对DIMA动态重构的架构基础、行为细节等要素进行建模。在此基础上, 设计了一种基于形式化定义的模型转换规则, 该规则将AADL动态重构模型转换成可执行的时间自动机模型。最后, 利用模型验证工具UPPAAL验证了可重构DIMA系统逻辑及时序的正确性和不安全控制行为的可达性。结果表明, 所提方法具有可行性和有效性, 并且能够为后续DIMA动态重构的形式化安全性评估提供模型基础。

来源：2022年第4期

《系统工程与电子技术》期刊编辑部

查看系统工程与电子技术杂志2022年第4期