Synthesized verification method for the inter-partition communication in IMA system integration

With the number of the functions of an avionics system increases continuously, the traditional federated avionics architecture cannot fulfill the functional requirements within expected volume and weight limitation. The application of Integrated Modular Avionics (IMA) architecture enables dramatical decrease in the weight, volume and power consumption of avionics system while all the desired functions are included. This is achieved by resource sharing in both time and space domain. The concept in the core of resource sharing is the partition mechanism, which is used as a technique to isolate errors in real-time operating system. However the side-effect of this mechanism is to propagate error through the communication between partitions. How to cut off the inter-partition error propagation is a challenging problem, which is also important for the implantation of IMA architecture. As such, the validation of inter-partition communication is the most effective measure to guarantee the error propagation. However, the traditional dynamic testing as a validation method for avionics system cannot fulfill this purpose because of the unacceptably large volume of the system state space. This paper proposes a synthesized validation method based on communication object exchange, which combined dynamic testing and formal verification. The method shows effectiveness according our research. The design of the inter-partition communication testing case is exemplified and the indispensability of formal verification is discussed.