Formal verification for inter-partitions communication of RTOS supporting IMA

Abstract

The IMA (Integrated Modular Avionics) architecture is widely used to support multi avionics applications and execute those applications independently. It is important to ensure the fault containment and ease of verification and certification in IMA. However during the inter-partitions communication, because it is performed by copying a message between kernel memory areas, it is possible to break the wall to prevent any partitioned function from causing a failure in another partitioned function. In this paper, we show the possibility of the error propagation in the IMA and verify the properties in the inter-partition communication module of Qplus-653 kernel.