Skip to Main content Skip to Navigation
Journal articles

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.
Complete list of metadata

Cited literature [43 references]  Display  Hide  Download

https://hal.inria.fr/hal-01262658
Contributor : Yliès Falcone <>
Submitted on : Wednesday, January 27, 2016 - 7:29:14 AM
Last modification on : Tuesday, May 11, 2021 - 11:37:32 AM
Long-term archiving on: : Thursday, April 28, 2016 - 11:14:51 AM

File

sttt3-rebip-Falcone-Jaber.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01262658, version 1

Collections

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⟩

Share

Metrics

Record views

578

Files downloads

493