Fully-automated Runtime Enforcement of Component-based Systems with Formal and Sound Recovery

Abstract : We introduce runtime enforcement of specifications on component-based systems (CBS) modeled in the BIP (Behavior, Interaction and Priority) framework. Runtime enforcement is an increasingly popular and effective dynamic validation technique aiming to ensure the correct runtime behavior (w.r.t. a formal specification) of a system using a so-called enforcement monitor. BIP is a powerful and expressive component-based framework for the formal construction of heterogeneous systems. Because of BIP expressiveness however , it is difficult to enforce complex behavioral properties at design-time. We first introduce a theoretical runtime enforcement framework for component-based systems where we delineate a hierarchy of enforceable properties (i.e., properties that can be enforced) according to the number of observational steps a system is allowed to deviate from the property (i.e., the notion of k-step enforceability). To ensure the observational equivalence between the correct executions of the initial system and the monitored system, we show that i) only stutter-invariant properties should be enforced on CBS with our monitors, and ii) safety properties are 1-step enforceable. Second, given an abstract enforcement monitor for some 1-step enforceable property, we define a series of formal transformations to instrument (at relevant locations) a CBS described in the BIP framework to integrate the monitor. At runtime, the monitor observes and automatically avoids any error in the behavior of the system w.r.t. the property. Third, our approach is fully implemented in RE-BIP, an available tool integrated in the BIP tool suite. Fourth, to validate our approach, we use RE-BIP to i) enforce deadlock-freedom on a dining philosophers benchmark, and ii) ensure the correct placement of robots on a map.
Type de document :
Article dans une revue
Software Tools for Technology Transfer (STTT), Springer, 2016
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01262658
Contributeur : Yliès Falcone <>
Soumis le : mercredi 27 janvier 2016 - 07:29:14
Dernière modification le : mercredi 11 avril 2018 - 01:51:58
Document(s) archivé(s) le : jeudi 28 avril 2016 - 11:14:51

Fichier

sttt3-rebip-Falcone-Jaber.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01262658, version 1

Citation

Yliès Falcone, Mohamad Jaber. Fully-automated Runtime Enforcement of Component-based Systems with Formal and Sound Recovery. Software Tools for Technology Transfer (STTT), Springer, 2016. 〈hal-01262658〉

Partager

Métriques

Consultations de la notice

376

Téléchargements de fichiers

152