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, 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.
Type de document :
Communication dans un congrès
8th International Symposium on Formal Aspects of Component Software - FACS 2011, Sep 2011, Oslo, Norway. Springer, 2011, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00642345
Contributeur : Olga Kouchnarenko <>
Soumis le : jeudi 17 novembre 2011 - 21:35:48
Dernière modification le : lundi 15 janvier 2018 - 14:24:07
Document(s) archivé(s) le : vendredi 16 novembre 2012 - 11:22:18

Fichier

facs2011_preproceedings_9.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. Springer, 2011, Lecture Notes in Computer Science. 〈hal-00642345〉

Partager

Métriques

Consultations de la notice

421

Téléchargements de fichiers

177