Verification of duration systems with one preemption

Summary form only given. Duration graphs are an extension of timed graphs supplied with a finite set of continuous real variables that can be stopped in some locations (rate=0) and resumed in other locations (rate=1). These variables are called: duration variables. Duration graphs are suitable for modelling real time schedulers with preemption which handle tasks that can be executed in parallel. However, the verification of reachability properties is undecidable for these graphs in dense time. We present a decidable class of duration graphs that we call large duration graphs with one preemption (ldg-1p for short). This class is suitable for modelling real time schedulers with one preemption where tasks cannot be interrupted more than once. In practice, a large number of real time schedulers fall into this class. We prove that the reachability problem is decidable for ldg-1p. In the first step of this proof, we present the digitization technique which consists to associate to every computation sequence of ldg-1p an integer computation sequence. Then, we demonstrate that this integer computation sequence is also a computation of the ldg-1p. We prove that solving the problem of decidability for ldg-1p in dense time is equivalent to solve it in integer time. Therefore, we propose to verify reachability properties in integer time where this problem is decidable. Finally, we present the decision method of the verification of reachability properties on ldg-1p.