关键词: 系统配置信息验证, MARTE, 模型驱动工程, ARINC653, 综合模块化航电系统（IMA）

Abstract: Recently, ensuring the correctness of system reconfiguration information is of great importance in safety and reliability of critical systems such as integrated modular avionics (IMA). This paper considers a configuration information model transformation and verification approach of IMA systems in the model-driven architecture with ARINC653 specification. Considering the features of IMA systems such as time or space multi-partition, this paper firstly defines a semantic mapping from the core elements of reconfiguration information (e.g. modules, partitions, memory, process and correspondence, etc.) to the MARTE model elements, and proposes a transformation approach between system configuration information and MARTE models. Then, this paper gives a formal verification framework based on the result MARTE models of system configuration information. Finally, a case study is illustrated to show the effectiveness of above proposed approach.

Key words: verification of system configuration information, MARTE, model driven engineering, ARINC653, integrated modular avionics (IMA)