Runtime Enforcement of Timed Properties

Srinivas Pinisetty 1 Yliès Falcone 2 Thierry Jéron 1 Hervé Marchand 1 Antoine Rollet 3 Omer Landry Nguena Timo 4
1 VERTECS - Verification models and techniques applied to testing and control of reactive systems
Inria Rennes – Bretagne Atlantique
2 VASCO
LIG - Laboratoire d'Informatique de Grenoble
3 LaBRI - Laboratoire Bordelais de Recherche en Informatique
4 IRIT - Institut de recherche en informatique de Toulouse
Abstract : Runtime enforcement is a powerful technique to ensure that a running system respects some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence that complies to a property. Runtime enforcement has been extensively studied over the last decade in the context of untimed properties. This paper introduces runtime enforcement of timed properties. We revisit the foundations of runtime enforcement when time between events matters.We show how runtime enforcers can be synthesized for any safety or co-safety timed property. Proposed runtime enforcers are time retardant: to produce an output sequence, additional delays are introduced between the events of the input sequence to correct it. Runtime enforcers have been prototyped and our simulation experiments validate their effectiveness.
Type de document :
Communication dans un congrès
3rd International Conference on Runtime Verification, Sep 2012, Istanbul, Turkey. Springer, 7687, pp.229-244, 2013, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-35632-2_23〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00743270
Contributeur : Hervé Marchand <>
Soumis le : lundi 19 novembre 2012 - 10:49:41
Dernière modification le : mercredi 23 mai 2018 - 17:58:06
Document(s) archivé(s) le : samedi 17 décembre 2016 - 12:23:28

Fichier

2012-RV-Enforcement.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

UNIV-TLSE2 | INRIA | LABRI | UNIV-BORDEAUX | LIG_GLSI_VASCO | LIG_GLSI | LIG | UNIV-TLSE3 | UGA | LIG_SRCPR | SMS

Citation

Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, Hervé Marchand, Antoine Rollet, et al.. Runtime Enforcement of Timed Properties. 3rd International Conference on Runtime Verification, Sep 2012, Istanbul, Turkey. Springer, 7687, pp.229-244, 2013, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-35632-2_23〉. 〈hal-00743270v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

559

Téléchargements de fichiers

105

Contact


archive-ouverte@inria.fr