Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components

Julien Dormoy 1 Olga Kouchnarenko 2 Arnaud Lanoix 3
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Dynamic reconfigurations increase the availability and the reliability of component-based systems by allowing their architectures to evolve at runtime. Recently we have proposed a temporal pattern logic, called FTPL, to characterize the correct reconfigurations of component-based systems under some temporal and architectural constraints. As component-based architectures evolve at runtime, there is a need to check these FTPL constraints on the fly, even if only a partial information is expected. Firstly, given a generic component-based model, we review FTPL from a runtime verification point of view. To this end we introduce a new four-valued logic, called RV-FTPL (Runtime Verification for FTPL), characterizing the "potential" (un)satisfiability of the architectural constraints in addition to the basic FTPL semantics. Potential true and potential false values are chosen whenever an observed behaviour has not yet lead to a violation or satisfiability of the property under consideration. Secondly, we present a prototype developed to check at runtime the satisfiability of RV-FTPL formulas when reconfiguring a Fractal component-based system. The feasability of a runtime property enforcement is also shown. It consists in supervising on the fly the reconfiguration execution against desired RV-FTPL properties. The main contributions are illustrated on the example of a HTTP server architecture.
Document type :
Conference papers
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-00642345
Contributor : Olga Kouchnarenko <>
Submitted on : Thursday, November 17, 2011 - 9:35:48 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM
Long-term archiving on : Friday, November 16, 2012 - 11:22:18 AM

File

facs2011_preproceedings_9.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00642345, version 1

Citation

Julien Dormoy, Olga Kouchnarenko, Arnaud Lanoix. Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components. 8th International Symposium on Formal Aspects of Component Software - FACS 2011, Sep 2011, Oslo, Norway. ⟨hal-00642345⟩

Share

Metrics

Record views

581

Files downloads

305