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)

摘要： 近年来，在以综合模块化航电系统（integrated modular avionics，IMA）为代表的一类安全关键应用中，确保系统重配置信息的正确性成为保证系统安全可靠运行的一个重要问题。提出了一种模型驱动架构下符合ARINC653规范的IMA系统配置信息的建模转换与验证方法。针对多个实时应用在IMA平台上以时间/空间多分区形式运行的系统特征，建立了从系统配置信息的核心元素（包括模块、分区、内存、进程、通信等）到MARTE模型元素的语义映射规则，设计了基于模型驱动架构的系统配置信息模型转换的方法，并给出了一种对模型转换构造得到的系统配置信息MARTE模型进行形式化验证的框架。最后，通过一个实例分析说明了此方法对验证重配置后系统配置信息的有效性。

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