Journal of Frontiers of Computer Science and Technology ›› 2015, Vol. 9 ›› Issue (4): 385-402.DOI: 10.3778/j.issn.1673-9418.1408014

Previous Articles     Next Articles

Model-Driven Reconfiguration Information Verification for Safety-Critical Systems

HU Jun1,2+, MA Jinjing1, LIU Xue1, CHENG Zhen1, SHI Jiaojie1, HUANG Zhiqiu1   

  1. 1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
    2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China
  • Online:2015-04-01 Published:2015-04-02

模型驱动的安全关键系统重配置信息验证方法

胡  军1,2+,马金晶1,刘  雪1,程  桢1,石娇洁1,黄志球1   

  1. 1. 南京航空航天大学 计算机科学与技术学院,南京 210016
    2. 南京大学 计算机软件新技术国家重点实验室,南京 210093

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)