Robust Analysis of Timed Automata

Nicolas Markey
LSV, Cachan, France
Friday, 26 October, 2007 (All day)
NO

Whereas formal verification of timed systems has become a very active field of research, the idealized mathematical semantics of timed automata cannot be faithfully implemented on digital, finite-precision hardwares. In particular, the properties proved on a timed automaton might not be preserved in any of its implementations.

In this talk, I will present one way of dealing with this problem, through an enlarged semantics of timed automata originally proposed in [DDR04]. I will first explain how to check implementability w.r.t. safety properties [DDMR04], and then extend this result to LTL properties [BMR06] and finally to a large fragment of MTL [BMR08].

(based on joint works with Martin De Wulf, Laurent Doyen, Jean-François Raskin, Patricia Bouyer and Pierre-Alain Reynier)

References:

  • [DDR04] Martin De Wulf, Laurent Doyen and Jean-François Raskin. Almost ASAP Semantics: From Timed Models to Timed Implementations. In Proceedings of the 7th International Workshop on Hybrid Systems: Computation and Control (HSCC'04), LNCS 2993. Springer-Verlag, 2004.
  • [DDMR04] Martin De Wulf, Laurent Doyen, Nicolas Markey and Jean-François Raskin. Robustness and Implementability of Timed Automata. In Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems, (FORMATS'04) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'04), LNCS 3253. Springer-Verlag, 2004.
  • [BMR06] Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier. Robust Model-Checking of Linear-Time Properties in Timed Automata. In Proceedings of the 7th Latin American Symposium on Theoretical INformatics (LATIN'06), LNCS 3887, pages 238-249. Springer-Verlag, 2006.
  • [BMR08] Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier. Robust Analysis of Timed Automata. Submitted. 2008.