Runtime enforcement of timed properties revisited

Abstract : Runtime enforcement is a powerful technique to ensure that a running system satisfies 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 with a property. Over the last decade, runtime enforcement has been mainly studied in the context of untimed properties. This paper deals with runtime enforcement of timed properties by revisiting the founda-tions of runtime enforcement when time between events matters. We propose a new enforce-ment paradigm where enforcement mechanisms are time retardants: to produce a correct output sequence, additional delays are introduced between the events of the input sequence. We consider runtime enforcement of any regular timed property defined by a timed automa-ton. We prove the correctness of enforcement mechanisms and prove that they enjoy two usually expected features, revisited here in the context of timed properties. The first one is soundness meaning that the output sequences (eventually) satisfy the required property. The second one is transparency, meaning that input sequences are modified in a minimal way. We also introduce two new features, i) physical constraints that describe how a time retar-dant is physically constrained when delaying a sequence of timed events, and ii) optimality, meaning that output sequences are produced as soon as possible. To facilitate the adoption and implementation of enforcement mechanisms, we describe them at several complemen-tary abstraction levels. Our enforcement mechanisms have been implemented and our ex- perimental results demonstrate the feasibility of runtime enforcement in a timed context and the effectiveness of the mechanisms.
Type de document :
Article dans une revue
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01088136
Contributeur : Hervé Marchand <>
Soumis le : jeudi 27 novembre 2014 - 14:36:08
Dernière modification le : mercredi 11 avril 2018 - 01:59:58
Document(s) archivé(s) le : vendredi 14 avril 2017 - 21:55:48

Fichier

fmsd2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Srinivas Pinisetty, Yliès Falcone, T Jéron, Hervé Marchand, Antoine Rollet, et al.. Runtime enforcement of timed properties revisited. Formal Methods in System Design, Springer Verlag, 2014, 45 (3), pp.381-422. 〈http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s10703-014-0215-y〉. 〈10.1007/s10703-014-0215-y〉. 〈hal-01088136〉

Partager

Métriques

Consultations de la notice

418

Téléchargements de fichiers

571