Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Robustness and Implementability of Timed Automata
du groupe Modélisation et Verification

Date 2012-01-12  11:30-12:30
TitreRobustness and Implementability of Timed Automata 
RésuméTimed automata are a well established model in real-time system design. They offer an automata-theoretic framework to design, verify and synthesize systems with timing constraints. The theory behind timed automata has been extensively studied and mature model-checking tools are available. However, this model makes unrealistic assumptions on the system, such as the perfect continuity of clocks and instantaneous reaction times, which are not preserved in implementation even in digital hardware with arbitrary finite precisions. While these assumptions are natural in the design phase, they must be validated before implementing the system. In this talk, I will first outline recent results on robustness analysis of timed automata, that is, deciding/computing an upper bound on the imprecisions under which a given property holds. I will then concentrate on the implementability problem, by presenting algorithms that render timed automata implementable: given a timed automaton, the goal is to construct a new timed automaton whose behavior under imprecisions is equivalent to the behavior of the first automaton. Based on joint works with Patricia Bouyer, Kim Larsen, Nicolas Markey, Claus Thrane.  
Lieu076 
OrateurOcan Sankur 
Emailocan.sankur@ens-cachan.fr 
UrlLSV, ENS Cachan 



Aucun document lié à cet événement.

Retour
Retour à l'index