Research On Integrated Modular Avionics System Configuration Verifications Based On MARTE

With the development of aviation electronic system, Integrated Modular Avionics(IMA) has become a kind of critical operating system. The ARINC653 standard is an industry standard that defines a set of services for the design of IMA. The standard defines a general-purpose APEX(APplication/EXecutive) interface between the Operating System(O/S) of an avionics computing resource and the application software. The IMA system which implements ARINC653 standard is called ARINC653 system. Configuration of IMA systems is a key technology that makes such systems flexible, yet controlled by dealing with the parameter of the hardware interface, O/S, and application program in the IMA system and configuration data contains all relative information on layers of the whole software architecture. In this case, the ability to verify configuration data is critical for quality assurance of ARINC653 system.In this paper, we consider verification on configuration of ARINC 653 system and schedulability of ARINC653 multitasking real-time systems based on Modeling and Analysis of Real-Time and Embedded systems(MARTE) and the details are listed below:1) Based on model driven architecture for IMA systems, we define a semantic mapping from core configuration elements(i.e., modules, partitions, memory, process, communication etc.) to elements in MARTE and propose a formalism for model translation of configuration based on MARTE.2) We propose a formalism for accuracy verification requirements description and develop a framework of MARTE model of system configuration; constraints requirements for model checking configuration are described in REAL theorem. This serves to detect errors of configuration and improve safety and reliability of systems.3) We focus on schedulability analysis of ARINC653 multitasking real-time systems. First, hierarchical scheduling strategies are described in MARTE according to the characters of ARINC653 partition system and then leverage a scheduling analyzer, called MAST to realize schedule analysis.4) We develop an assistant tool, called Configuration Checker for ARINC653(CC653) for modeling and verification configuration and scheduling on Papyrus modeling platform. We implement our approach and illustrate its effectiveness on a benchmark from literature.