一种基于AADL的IMA系统配置信息的正确性检测方法

Correctness Verification for Integrated Modular Avionics System Configuration Based on AADL Model

综合模块化航空电子系统(Integrated modular avionics,IMA)中的系统配置信息的正确性是保证IMA系统可靠运行的重要保障。配置信息的重配置给系统的更新和移植提供了方便,同时也给重配置后的系统带来了不安全因素。本文针对满足ARINC653规范的IMA系统重配置信息的正确性检测方法,展开了基于架构分析和设计语言(AADL)模型转换与分析的研究。给出了一系列从ARINC653系统配置信息到AADL模型元素的映射规则,包括模块、分区、进程、健康监控、通信等核心概念,并设计了一个模型转换的方法,然后采用一个第三方的工具对所得到的AADL模型展开配置信息正确性的语义验证。最后本文还给出了一个实例分析。

The configuration information correctness of the integrated modular avionics （IMA） system is an important guarantee of operational reliability.Reconfiguration of configuration information provides conveniences for system updating and transplantation,and brings unsafe factors to system.Concerning the detection method for the correctness of the IMA system which satisfies ARINC653 specification,the transformation and analysis of the architecture analysis and design language （AADL） model are researched.Elements mapping rules from ARINC653 system configuration information to the AADL model are proposed,including module,partition,process,health,monitoring,communication and other core concepts.A model transformation approach is given,and a formal semantic verification of the configuration information correctness of AADL model is presented based on a third-party tool.Finally,an example analysis is provided.