Partager cette page :

On the Modeling and Verification of Timed systems

le 31 janvier 2012

de 15h30 à 17h00

ENS Rennes Salle du conseil
Plan d'accès

Intervention en anglais d'Akshay Sundararaman, actuellement postdoctorant à l'ENS Cachan - Bretagne (séminaire du département Informatique et télécommunications).

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.

Formation, Recherche - Valorisation
Claude Jard

Mise à jour le 12 septembre 2019