Abstract
Timed systems are those for which constraints linked to physical time are essential for correct operation: real-time embedded systems, communication protocols directly dependent on time or subject to transmission delay constraints, etc. A standard formalism for describing them is that of timed automata, whose transitions can be governed by variables called clocks. A standard formalism to describe them is that of timed automata, whose transitions can be governed by variables called clocks. These variables all advance at the same rate as a function of time, they condition transitions, and they can be individually reset to zero during transitions. Based on examples written using the UPPAAL system described later in the seminar, we present the formalism and how to express the properties to be verified. We then describe algorithms for efficiently deciding the properties of timed automata. These algorithms, which are geometric in nature, study the mutual constraints that the automaton imposes on the clocks, either exactly or by abstract interpretation. They translate the initial verification problem into sets of inequalities at clock differences, whose satisfiability can be decided with fast algorithms, also used in the SMT systems described in the previous lecture.
