Formal Verification of the Inter-core Synchronization of a Multi-core RTOS Kernel

Checking compliance of a Real-Time Operating System (RTOS) with the standard it is supposed to implement is usually achieved by executing a test suite. That is, for example, the case for OS conforming to the AUTOSAR standard. The task becomes complex for multi-core implementations because simultaneous executions are usually not tested and are, in any case, difficult to test generically as the possible interleaving depends on the execution speeds of the cores. In this paper, we propose to use model-checking to verify the communication and synchronization mechanisms involved in the concurrent execution of OS services: concurrent accesses to OS data structures, multi-core scheduling, and inter-core interrupt handling. The multi-core operating system and the application are modeled by a High-level Colored Time Petri Nets (HCTPN) reproducing the control flow graph and using the same variables as the actual implementation. This approach allows to verify compliance with some standards. This paper focuses on rare situations with simultaneous service calls in parallel on several cores that are almost impossible to test on real implementation but that we will be able to obtain by our model checking method. We applied our approach to an OSEK and AUTOSAR compliant RTOS called Trampoline.