Research On Reconfiguration And Verification Methods For Integrated Modular Avionics

In order to meet the growing military and civilian needs of aircraft,Integrated Modular Avionics(IMA)has received intensive research in recent years.It is a safety-critical embedded system.When the operating environment is changed or the component fails,the software and hardware resources are reconfigured to ensure functional and performance requirements.Reconfiguration must be performed strictly in accordance with pre-defined policies to avoid out of control and failures.Therefore,to ensure the functional requirements and safety of the system in the reconfiguration design process,how to allocate the resources of the IMA system is the key to the normal operation of the aircraft.Although there are many achievements in the reconfiguration design of IMA,the existing methods still face the following challenges.First,system reconfiguration is a remapping of logical architecture to physical implementation.Due to the diversity and uncertainty of the process and the lack of accurate description of resources,it is difficult to collect software and hardware resources information.The degree of reconfiguration automation is low.Secondly,the existing verification methods have different emphasis on system logic model,system physical model and partition mapping.They lack the necessary connection.There are no unified mapping relations between models,and the integrity of verification results needs to be improved.The mapping process is simplified by the model-based reconstruction method.The functional and safety requirements are verified,and the configuration of system resources is realized.Therefore,it has certain practical significance.In this thesis,the methods of system modeling,mapping,verification,blueprint generation are researched.The main contributions of this thesis include:(1)To ensure the logic architecture of the reconfigured system meets the functional requirements,an automaton model construction and verification approach for System Modeling Language(Sys ML)activity diagram is proposed.The extended finite automaton model is used to model the content and nested calls of activity diagrams,and the linear-time temporal logic is used to represent the functional requirement attributes.Then the consistency of functional logic flow and requirements is verified by conversion algorithm and model checking.A model-based test case generation approach is proposed.As test models,the extended constraint interface automata are used to describe the correct activity diagrams.Optimistic approach and game theory are used to model the nested calls among activities.Then the coverage criteria of flow constraint condition combination are defined,and the algorithm for test cases generating is given to automatically generate test cases for functional testing of the architecture.(2)To ensure the logic architecture of the reconfigured system meets the safety requirements,a model-based system safety requirements description and verification approach is proposed.Hazard use cases are established and safety requirements are captured according to the system functional requirements,safety objectives,and failure states.Then the state machine diagrams with functional failure are used to describe the system functional model including safety requirements.The safety extended hierarchical automata are used as the intermediate models,and the formal description of the system functional model is realized by the transformation algorithm.The safety requirement verification is completed by the model checking.(3)To ensure the physical architecture of the reconfigured system meets the safety requirements,a model-based component error behavior description and verification approach is proposed.The physical architecture models are established according to system functional requirements and safety objectives,and the error model annex is used to describe the error behavior and failure effects for components.Then the hierarchical automata are used as the intermediate state,and the formal description of the physical architecture error behavior model is realized by the transformation algorithm.Finally,whether the designed component error effect and response measures meet the safety objectives of the system are verified by model checking.(4)To ensure the efficiency and quality of system reconfiguration,a model-based system reconfiguration approach is proposed.The composition of system logic function is divided into several levels.The mapping rules for the logical architecture model to the AADL components,and the AADL components to the ARINC653 elements are realized.The mode is used to represent the system runtime resource configuration.System reconfigurations at different levels are realized through mode migration.Then the architecture models are analyzed and verified.A blueprint for reconfiguration is formulated to guide the dynamic configuration of system resources.