Fully-automated Runtime Enforcement of Component-based Systems with Formal and Sound Recovery - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Journal Articles International Journal on Software Tools for Technology Transfer Year : 2016

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.
Fichier principal
Vignette du fichier
sttt3-rebip-Falcone-Jaber.pdf (995.22 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01262658 , version 1 (27-01-2016)

Identifiers

  • HAL Id : hal-01262658 , version 1

Cite

Yliès Falcone, Mohamad Jaber. Fully-automated Runtime Enforcement of Component-based Systems with Formal and Sound Recovery. International Journal on Software Tools for Technology Transfer, 2016. ⟨hal-01262658⟩
319 View
220 Download

Share

Gmail Facebook X LinkedIn More