Nicolas Markey

Résumé

Timed automata are governed by a mathematical semantics which assumes perfectly continuous and precise clocks. This requirement is not satised by digital hardware on which the models are implemented. In fact, it was shown that the presence of imprecisions, however small they may be, may yield extra behaviours. Therefore correctness proven on the formal model does not imply correctness of the real system.

The problem of robust model-checking was then dened to circumvent this inconsistency. It consists in computing a bound on the imprecision under which the system will be correct.

In this work, we show that robust model-checking against ω-regular properties for timed automata can be reduced to standard model-checking of timed automata, by computing an adequate bound on the imprecision. This yields a new algorithm for robust model-checking of ω-regular properties, which is both optimal and valid for general timed automata.

@inproceedings{formats2011-BMS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
                         Ocan},
  title =               {Robust Model-Checking of Timed Automata via Pumping
                         in Channel Machines},
  editor =              {Fahrenberg, Uli and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'11)},
  acronym =             {{FORMATS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6919},
  pages =               {97-112},
  year =                {2011},
  month =               sep,
  doi =                 {10.1007/978-3-642-24310-3_8},
  abstract =            {Timed automata are governed by a mathematical
                         semantics which assumes perfectly continuous and
                         precise clocks. This requirement is not satised by
                         digital hardware on which the models are
                         implemented. In~fact, it~was shown that the presence
                         of imprecisions, however small they may be, may
                         yield extra behaviours. Therefore correctness proven
                         on the formal model does not imply correctness of
                         the real system.\par The problem of robust
                         model-checking was then dened to circumvent this
                         inconsistency. It consists in computing a bound on
                         the imprecision under which the system will be
                         correct.\par In this work, we show that robust
                         model-checking against \(\omega\)-regular properties
                         for timed automata can be reduced to standard
                         model-checking of timed automata, by computing an
                         adequate bound on the imprecision. This yields a new
                         algorithm for robust model-checking of
                         \(\omega\)-regular properties, which is both optimal
                         and valid for general timed automata.},
}