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.