Research On Model-Driven Analysis And Verification Of System Configuration For Integrated Modular Avionics

System configuration of integrated modular avionics(IMA) is the core content in avionicssystem, which holds the parameters of the system software, hardware and all system components’ information. Wrong configuration can lead to abnormal operation of system and bring the tragedy in the plane crash. At the same time, in order to meet the real-time requirements of system, it’s import that make sure system tasks to complete. As a result, before using IMAsystem configuration, relibable and schedulable verification of configuration information is very important. Model driven engineering(MDE), which is based on model, through the analysis,design, build and test of model, implement the relibable and schedulable verification of safety critical systems. Architecture design and analysis of language(AADL) is the language whichis accorded with the idea of MDE. It is effective for safety ciritical systems modeling design and analysis and has been widely used in the field of avionics systems.Against the proposed the system reliable and schedulable verification issues of the configuration information, this paper puts forward the analysis and verification of the configuration information based on MDE. The main research content is as follows:(1) Research on model transformations in model-driven content, analysis of the semanticsimilarity between configuration information and AADL model elements, the transformation rules between AADL model elements and seven major core concepts(module, partition, process, intra-partition communication, inter-partition communication, health monitor) of configuration. Based on the rules of these transformations, this paper constructs the transformation method from configuration to AADL model.(2) Research on the model verification language REAL and the design rules of REAL theorem, according to the reliability verification requirements of configuration information, useREAL to design the corresponding relibability verification theorem. This paper constructs therelibability verification method for the generated AADL model based on the model analysis suite Ocarina.(3) Research on the partition tasks’ scheduling model of IMA system and the method ofCheddar custom scheduling policy, based on schedulability verification requirements of configuration information, use Cheddar to design partition tasks’ scheduling strategy. This paper constructs the schedulability verification method for the generated AADL model base on simulation.(4) Design the configuration analysis and verification tool ARINC653Verification which have reliability verification function of configuration information. The tool mades up of two sub-modules: model transformation module, through input ARINC653configuration file, outputAADL model file; through input the generated AADL model and the REAL theorems whichvalidate the reliability of configuration information, output verification results.(5) Give the instance of analysis and verification method of system configuration information, including: the XML file content of the instance; Conversion generated AADL model filecontent; reliability verification results of configuration information; simulation gantt chart of system tasks and worst-case response time of system tasks, schedulability verification results ar e given.