Time: Wednesday 18.8.2004, 14:30
Place: Room A4-106, Fr. Bajersvej 7
In this talk we address the issue of the verification of real-time
systems using time Petri nets. Our approach is translation-based: Given
a bounded time Petri net, we compute its state space as a timed
automaton, whose low number of clocks allows efficient verification
with tools like Uppaal.
This approach is then extended to a superclass of time Petri nets, featuring stopwatches and dedicated to the modeling of preemptive scheduling. This yields a stopwatch automaton, which can be verified using HyTech for instance. While computing the state space of models involving stopwatches typically requires the (time and memory very demanding) use of general form convex polyhedra, we show that our translation can be achieved using a particular subclass of polyhedra known as Difference Bounds Matrices and for which efficient handling algorithms are known. This contributes greatly to the efficiency of the approach, which allows us to practically verify much larger systems than a direct modeling as a product of stopwatch automata.