Combining Proof and Model-checking to Validate Reconfigurable Architectures

Arnaud Lanoix 1 Julien Dormoy 2 Olga Kouchnarenko 3
3 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 : This paper deals with the formal specification and verification of dynamic reconfigurations of component-based systems. To validate such complex systems, there is a need to check model consistency and also to ensure that dynamic reconfigurations satisfy architectural and integrity constraints, invariants, and also temporal constraints over (re)configuration sequences. As architectural constraints involve first-order formulas, and a behavioral semantics of reconfigurations gives rise to infinite state systems, we propose to associate proof and model-checking within the well-established B method, to support the modeling of such systems and the (partial-)validation of their dynamic reconfigurations. The objective of the paper is twofold. First, given a hierarchical B model of component-based architectures, we validate it by proving its consistency. Second, given linear temporal logic formulas expressing the desirable dynamic behavior of the system, we validate reconfigurable system architectures by using bounded model-checking tools supporting the B method. The main contributions are illustrated on the example of a HTTP server architecture.
Type de document :
Communication dans un congrès
8th International Workshop on Formal Engineering approaches to Software Components and Architectures - FESCA 2011, joint to ETAPS 2011, Apr 2011, Saarbrucken, Germany. 279(2), pp.43-57, 2011, Electr. Notes Theor. Comput. Sci. 〈http://dx.doi.org/10.1016/j.entcs.2011.11.011〉. 〈10.1016/j.entcs.2011.11.011〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00642348
Contributeur : Olga Kouchnarenko <>
Soumis le : jeudi 17 novembre 2011 - 21:50:34
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral

Identifiants

Citation

Arnaud Lanoix, Julien Dormoy, Olga Kouchnarenko. Combining Proof and Model-checking to Validate Reconfigurable Architectures. 8th International Workshop on Formal Engineering approaches to Software Components and Architectures - FESCA 2011, joint to ETAPS 2011, Apr 2011, Saarbrucken, Germany. 279(2), pp.43-57, 2011, Electr. Notes Theor. Comput. Sci. 〈http://dx.doi.org/10.1016/j.entcs.2011.11.011〉. 〈10.1016/j.entcs.2011.11.011〉. 〈hal-00642348〉

Partager

Métriques

Consultations de la notice

367