Expressiveness and analysis of scheduling extended time Petri nets

International audienceThe most widely used approach for verifying the schedulability of a real-time system consists of using analytical methods. However, for complex systems with interdependent tasks and variable execution times, they are not well adapted. For those systems, an alternative approach is the formal modelisation of the system and the use of model-checking, which also allows the verification of more varied scheduling properties. In this paper, we show how an extension of time Petri nets : scheduling extended time Petri nets (SETPN), is especially well adapted for the modelisation of real-time systems and particularly embedded systems and we provide a method for computing the state space of SETPN. We first propose an exact computation using a general polyhedron representation of time constraints, then we propose an overapproximatiion of the polyhedra to allow the use of much more efficient data structures, DBMs. We finally describe a particular type of observers, that gives us a numeric result (instead of boolean) for the computation of tasks response times