Safety Analysis And Verification For Resource Configuration In Integrated Modular Avionics System Based On AADL

Resource allocation is a significant part of integrated modular avionics system(IMA) design, the system configuration information is also an important content of avionics system, which stores the parameters of the system software and hardware. The wrong configuration information can lead to abnormal operation of system and even lead to a large accident, so it is important to analyse the security of the configuration information, especially the verification of reliability and schedulability. With the increasing complexity of embedded systems and the continuous improvement of security requirements, model driven engineering(MDE), which is based on model, has become the mainstream. And AADL is a new standard for embedded real-time system, it can better support the establishment of the model of embedded system software and hardware, and also can describe the non functional properties of the system reliability, real-time, and so on. So it has been widely used in the field of aviation electronic systems.In view of reliability and schedulability verification of IMA system configuration information and the security analysis of the IMA system, the main work of this paper is as follows:(1) The semantics similarity of the AADL model elements and ARINC653 configuration information are respectively analyzed. The transformation rules of the key concepts of the configuration information and the AADL model elements are provided. Then use the rules to convert the configuration information into AADL model, and use REAL to design the corresponding relibability verification theorem.(2) The AADL model is analyzed, using the time automata formal analysis method to design thread timed automata templates and scheduler timed automata templates. And the mapping semantic between AADL scheduling model and timed automaton model is given to convert the AADL model into a time automaton model. According to the requirement of scheduling verification of the configuration information, the timed automate model is simulated and verified in the tool UPPAAL to analyse whether the original AADL model meets schedulability qualities.(3) Using Eclipse plug-in development technology to design configuration conversion and verification tool, and integrate it into the AADL modeling and analysis tool OSATE, the tool has following functions: Input configuration information file and convert it into AADL model, then combine with the REAL theorem and Ocarina tool to verify the reliability of the configuration information; through file parsing, convert and generate time automaton model file and property verification query file, and automatically open the UPPAAL tool to verify the schedulability of the model. And at last, an example is also given to verify the correctness of the tool.(4) On the basis of configuration information AADL model, the model of application layer and function layer are established in OSATE tool, and the failure model is established based on AltaRica language and the fault tree is researched using SimFia tool.