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

来源：系统工程与电子技术杂志2022年第4期北京时间：

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

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

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

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

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