On the Modeling and Verification of Timed systems

The model checking paradigm involves automatically verifying properties about real-life systems by abstracting them into mathematical models. For modeling complex real-life systems, like embedded systems or communication protocols, one often requires to be able to express and verify quantitative properties (like the delay between two events is no more than 5ms) to ensure that the system behaves as expected. Timed automata, which equip regular finite state automata with clocks, have been proposed in the early nineties as a model for real-time systems with nice theoretical properties. 

In this talk, we will present some basics of timed automata as well as a few theoretical results regarding them. We will then discuss a more recent extension to a distributed setting, where several timed automata interact using clocks that evolve independently of each other.