Fulltext

Robust safety of timed automata

De Wulf, Martin ; Doyen, Laurent ; Markey, Nicolas ; Raskin, Jean-François

In: Formal Methods in System Design, 2008, vol. 33, no. 1-3, p. 45-84

Ajouter à la liste personnelle
    Titre
    • Robust safety of timed automata
    Auteur
    • De Wulf, Martin. Dépt Informatique, Université Libre de Bruxelles (ULB), Campus de la Plaine, Bd du Triomphe CP 212, 1050, Brussels, Belgium
    • Doyen, Laurent. École Polytechnique Fédérale de Lausanne (EPFL), Station 14, 1015, Lausanne, Switzerland
    • Markey, Nicolas. Laboratoire Spécification & Vérification (LSV), ENS Cachan & CNRS, 61 av. Pdt Wilson, 94230, Cachan, France
    • Raskin, Jean-François. Dépt Informatique, Université Libre de Bruxelles (ULB), Campus de la Plaine, Bd du Triomphe CP 212, 1050, Brussels, Belgium
    Type de document
    • Postprint
    Langue
    • Anglais
    Publié dans
    • Formal Methods in System Design, 2008, vol. 33, no. 1-3, p. 45-84. Springer US; http://www.springer-ny.com
    Autre version électronique
    Identifiant OAI-PMH
    • oai:doc.rero.ch:321009
    Summary
    Timed automata are governed by an idealized semantics that assumes a perfectly precise behavior of the clocks. The traditional semantics is not robust because the slightest perturbation in the timing of actions may lead to completely different behaviors of the automaton. Following several recent works, we consider a relaxation of this semantics, in which guards on transitions are widened byΔ>0 and clocks can drift byε>0. The relaxed semantics encompasses the imprecisions that are inevitably present in an implementation of a timed automaton, due to the finite precision of digital clocks. We solve the safety verification problem for this robust semantics: given a timed automaton and a set of bad states, our algorithm decides if there exist positive values for the parametersΔ andε such that the timed automaton never enters the bad states under the relaxed semantics