
Timed Models: From Theory to Implementation 
Patricia Bouyer
(LSVCNRS and ENS of Cachan, France)

Duration: 90 minutes 
ABSTRACT:
Many critical applications have explicit timing constraints. For
example, behaviours of systems interacting with an environment (e.g.
embedded systems) depend on quantitative timing constraints like
response times, transmission delays, etc. For representing such timed
systems, several timed models have been proposed. Since their
introduction by Alur and Dill in the 90s, timed automata are one of the
moststudied and mostestablished models for realtime systems. Numerous
works have been devoted to the comprehension of timed automata and the
major property of timed automata is probably that reachability is
decidable, which implies in particular that it can be used for
verification purposes. Based on this nice theoretical result, several
modelcheckers have been developed (for instance CMC, HyTech, Kronos and
Uppaal) and a lot of case studies have been treated.
Decidability properties for timed automata are proved based on the
construction of the socalled region automaton: it abstracts finitely
and in a correct way the behaviours of timed automata. However, in
practice, such a construction is not implemented, because it suffers
from an enormous combinatorics explosion, but algorithms searching
onthefly through the automaton are preferred. These algorithms are
based on the notion of zones and can be efficiently implemented using
data structures like DBMs. Among these algorithms are the forward
analysis algorithms that compute all the reachable configurations from
the initial configurations. However, the exact forward computation does
not always terminate. Abstractions have to be used to avoid this
termination problem but one has to be careful when using such abstractions.
In this tutorial, we will present basic results on timed automata as
well as abstractions and algorithms that are used in practice.
 