Didier Lime

Institut de Recherche en Communications et en Cybernétique de Nantes, University of Nantes, France.

Time: Wednesday 18.8.2004, 14:30
Place: Room A4-106, Fr. Bajersvej 7

Timed analysis of real-time systems using extended time Petri nets

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.