Skip to Main content Skip to Navigation
New interface
Conference papers

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Olga Kouchnarenko Connect in order to contact the contributor
Submitted on : Thursday, November 17, 2011 - 9:35:48 PM
Last modification on : Wednesday, April 27, 2022 - 3:49:18 AM
Long-term archiving on: : Friday, November 16, 2012 - 11:22:18 AM


Files produced by the author(s)


  • HAL Id : hal-00642345, version 1


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⟩



Record views


Files downloads