基于形式化方法的DIMA动态重构仿真与验证

作     者：刘嘉琛 董磊 赵长啸 陈泓兵 LIU Jiachen;DONG Lei;ZHAO Changxiao;CHEN Hongbing

作者机构：中国民航大学安全科学与工程学院天津300300 中国民航大学民航航空器适航审定技术重点实验室天津300300 天津市民用航空器适航与维修重点实验室天津300300 

出 版 物：《系统工程与电子技术》 (Systems Engineering and Electronics)

年 卷 期：2022年第44卷第4期

页      面：1282-1290页

核心收录：

学科分类：08[工学] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

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

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