Evènement pour le groupe Modélisation et Verification
|Date|| 2012-01-12 11:30-12:30|
|Titre||Robustness 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.
|Orateur||Ocan Sankur |
|Url||LSV, ENS Cachan |
Aucun document lié à cet événement.RetourRetour à l'index