May 15, 2023
Imane Haur (EC Nantes, Sogeti)Formal verification is a solution to increase the system’s implementation reliability. In our work, we are interested in using these methods to verify multi-core RTOS. We propose a model-checking approach using time Petri nets extended with colored transitions and high-level features. We use this formalism to model the Trampoline multi-core OS, compliant with the OSEK/VDX and AUTOSAR standards. We first define this formalism and show its suitability for modeling real-time concurrent systems. We then use this formalism to model the Trampoline multi-core RTOS and verify by model-checking its conformity with the AUTOSAR standard. From this model, we can verify properties of both the OS and the application, such as the schedulability of a real-time system and the synchronization mechanisms: concurrent access to the data structures of the OS, multi-core scheduling, and inter-core interrupt handling. As an illustration, this method allowed the automatic identification of two possible errors of the Trampoline OS in concurrent execution, showing insufficient data protection and faulty synchronization.