Enforcement of (Timed) Properties with Uncontrollable Events

Matthieu Renard 1 Yliès Falcone 2, 3 Antoine Rollet 1 Srinivas Pinisetty 4 Thierry Jéron 5 Hervé Marchand 5
1 LaBRI - Laboratoire Bordelais de Recherche en Informatique
2 CORSE - Compiler Optimization and Run-time Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
3 LIG - Laboratoire d'Informatique de Grenoble
4 Aalto University
5 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper deals with runtime enforcement of untimed and timed properties with uncontrollable events. Runtime enforcement consists in modifying the executions of a running system to ensure their correctness with respect to a desired property. We introduce a framework that takes as input any regular (timed) property over an alphabet of events, with some of these events being uncontrollable. An uncontrollable event cannot be delayed nor intercepted by an enforcement mechanism. Enforcement mechanisms satisfy important properties, namely soundness and compliance, meaning that enforcement mechanisms output correct executions that are close to the input execution. We discuss the conditions for a property to be enforceable with uncontrollable events, and we define enforcement mechanisms that modify executions to obtain a correct output, as soon as possible. Moreover, we synthesize sound and compliant descriptions of runtime enforcement mechanisms at two levels of abstraction to facilitate their design and implementation.
Type de document :
Communication dans un congrès
12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), Oct 2015, Cali, Colombia. Springer, LNCS (9399), pp.22, 2015, Theoretical Aspects of Computing - ICTAC 2015. 〈10.1007/978-3-319-25150-9_31〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01185238
Contributeur : Antoine Rollet <>
Soumis le : jeudi 1 octobre 2015 - 11:37:32
Dernière modification le : jeudi 11 octobre 2018 - 08:48:05
Document(s) archivé(s) le : samedi 2 janvier 2016 - 10:59:16

Fichier

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

Licence

Copyright (Tous droits réservés)

Identifiants

Collections

INRIA | LIG | UGA | IRISA | UNIV-BORDEAUX | LABRI | LIG-SRCPR-CORSE | LIG_SRCPR | TDS-MACS | UR1-UFR-ISTIC | CENTRALESUPELEC | UNIV-RENNES

Citation

Matthieu Renard, Yliès Falcone, Antoine Rollet, Srinivas Pinisetty, Thierry Jéron, et al.. Enforcement of (Timed) Properties with Uncontrollable Events. 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), Oct 2015, Cali, Colombia. Springer, LNCS (9399), pp.22, 2015, Theoretical Aspects of Computing - ICTAC 2015. 〈10.1007/978-3-319-25150-9_31〉. 〈hal-01185238v3〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

722

Téléchargements de fichiers

130

Contact


archive-ouverte@inria.fr