| |
| Timed Models: From Theory to Implementation |
Patricia Bouyer
(LSV-CNRS 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
most-studied and most-established models for real-time 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
model-checkers 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 so-called 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
on-the-fly 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.
| |