Nicolas Markey

Résumé

Formal verification of timed systems is well understood, but their implementation is still challenging. Recent works by Raskin et al. have brought out a model of parameterized timed automata that can be used to prove implementability of timed systems for safety properties. We define here a more general notion of robust model-checking for linear-time properties, which consists in verifying whether a property still holds even if the transitions are slightly delayed or expedited. We provide PSPACE algorithms for the robust model-checking of Büchi-like and LTL properties. We also verify bounded-response-time properties.

@inproceedings{latin2006-BMR,
  author =              {Bouyer, Patricia and Markey, Nicolas and Reynier,
                         Pierre-Alain},
  title =               {Robust Model-Checking of Linear-Time Properties in
                         Timed Automata},
  editor =              {Correa, Jos{\'e} R. and Hevia, Alejandro and Kiwi,
                         Marcos},
  booktitle =           {{P}roceedings of the 7th {L}atin {A}merican
                         {S}ymposium on {T}heoretical {IN}formatics
                         ({LATIN}'06)},
  acronym =             {{LATIN}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3887},
  pages =               {238-249},
  year =                {2006},
  month =               mar,
  doi =                 {10.1007/11682462_25},
  abstract =            {Formal verification of timed systems is well
                         understood, but their \emph{implementation} is still
                         challenging. Recent works by Raskin \emph{et al.}
                         have brought out a model of parameterized timed
                         automata that can be used to prove
                         \emph{implementability} of timed systems for safety
                         properties. We define here a more general notion of
                         robust model-checking for linear-time properties,
                         which consists in verifying whether a property still
                         holds even if the transitions are slightly delayed
                         or expedited. We provide PSPACE algorithms for the
                         robust model-checking of B{\"u}chi-like and LTL
                         properties. We also verify bounded-response-time
                         properties.},
}