| 基于形式化方法的DIMA动态重构仿真与验证 |
| |
| 引用本文： | 刘嘉琛,董磊,赵长啸,陈泓兵. 基于形式化方法的DIMA动态重构仿真与验证[J]. 系统工程与电子技术, 2022, 44(4): 1282-1290. DOI: 10.12305/j.issn.1001-506X.2022.04.26 |
| |
| 作者姓名： | 刘嘉琛 董磊 赵长啸 陈泓兵 |
| |
| 作者单位： | 1. 中国民航大学安全科学与工程学院, 天津 3003002. 中国民航大学民航航空器适航审定技术重点实验室, 天津 3003003. 天津市民用航空器适航与维修重点实验室, 天津 300300 |
| |
| 基金项目： | 国家自然科学基金-民航联合基金(U1933106);航空科学基金(20185167017);中央高校基本科研业务费(3122019167) |
| |
| 摘 要： | 针对可重构分布式综合模块化航空电子(distributed integrated modular avionics,DIMA)系统在设计初期缺少仿真与验证手段的问题,首先分析了可重构DIMA软件体系的架构特征以及支持动态重构的层次化通用系统管理(generic system management,GSM)的组件功能划分...
|
| 关 键 词： | 分布式综合模块化航空电子 动态重构 架构分析与设计语言 形式化方法 仿真验证 |
| 收稿时间： | 2021-02-17 |
Simulation and verification of DIMA dynamic reconfiguration based on formal method |
| |
| Jiachen LIU,Lei DONG,Changxiao ZHAO,Hongbing CHEN. Simulation and verification of DIMA dynamic reconfiguration based on formal method[J]. System Engineering and Electronics, 2022, 44(4): 1282-1290. DOI: 10.12305/j.issn.1001-506X.2022.04.26 |
| |
| Authors: | Jiachen LIU Lei DONG Changxiao ZHAO Hongbing CHEN |
| |
| Affiliation: | 1. College of Safety Science and Engineering, Civil Aviation University of China, Tianjin 300300, China2. Key Laboratory of Civil Aircraft Airworthiness Technology, Civil Aviation University of China, Tianjin 300300, China3. Civil Aircraft Airworthiness and Repair Key Laboratory of Tianjin, Tianjin 300300, China |
| |
| Abstract: | In view of the lack of simulation and verification means in the early design stage of reconfigurable distributed integrated modular avionics (DIMA) system, the architecture characteristics of reconfigurable DIMA software system and the component function division of hierarchical generic system management (GSM) supporting dynamic reconfiguration are analyzed firstly. Then, architecture analysis and design language (AADL) and its related accessories are used to model the architectural basis, behavior details and other elements of DIMA dynamic reconfiguration. On this basis, a model transformation rule based on formal definition is designed, which transforms AADL dynamic reconstruction model into executable timed automata model. Finally, the correctness of logic and timing of reconfigurable DIMA system and the accessibility of unsafe control behavior are verified by using model verification tool UPPAAL. The results show that the proposed method is feasible and effective, and can provide a model basis for the formal security evaluation of subsequent DIMA dynamic reconfiguration. |
| |
| Keywords: | distributed integrated modular avionics (DIMA) dynamic reconfiguration architecture analysis and design language (AADL) formal method simulation verification |
|
| 点击此处可从《系统工程与电子技术》浏览原始摘要信息 |
|
点击此处可从《系统工程与电子技术》下载全文 |
|
