Model-Checking of Concurrent Real-Time Software Using High-Level Colored Time Petri Nets with Stopwatches

The control of real-time systems often requires taking into account simultaneous access in true parallelism to shared resources. This is particularly the case for multicore execution platforms. Timed automata or time Petri nets do not capture these features directly. We first define High-level Colored Time Petri Net (HCTPN) that extends time Petri Nets with color and high-level functionality encompassing both timed multi-enableness of transitions and sequential pseudo code. We then extend HCTPN with stopwatches to allow the modeling of preemptive scheduling, which is an important feature in the real-time context. We prove that the reachability problem is decidable for HCTPN but is undecidable for HCTPN with stopwatches, and we propose an abstraction of the state space for these models. We apply this approach to model a preemptive multi-core real-time application that uses a spinlock mechanism in order to check all possible execution paths, interleaving of service calls, and preemptive scheduling.