ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Autres revues >>

L'Objet

1262-1137
logiciel, bases de données, réseaux
Publication abandonné
 

 ARTICLE VOL 14/4 - 2008  - pp.73-102  - doi:10.3166/obj.14.4.73-102
TITRE
Une approche formelle de la reconfiguration dynamique

RÉSUMÉ
Les applications auto-adaptables modifient leur comportement de façon dynamique et autonome par le biais d'opérations d'introspection, de recomposition, d'ajout et suppression de composants, dans le but de s'adapter aux changements pouvant survenir dans leur contexte d'exécution. Un des moyens de favoriser leur robustesse est de disposer d'un support formel permettant de modéliser ces applications, de spécifier les programmes d'adaptation, d'y exprimer des propriétés et de les vérifier. Nous proposons un cadre formel de spécification et de raisonnement sur des programmes avec reconfiguration dynamique inspiré du modèle à composants Fractal. Le cadre proposé, nommé FracL, est fondé sur une description axiomatique des primitives de Fractal en logique de premier ordre, et permet la spécification et la preuve des propriétés autant fonctionnelles que de contrôle dans ces systèmes. Notre modèle a été traduit dans l'atelier de spécification et de preuve Focal, ce qui permet à la fois d'en assurer la cohérence et de fournir un cadre outillé pour raisonner sur des applications concrètes.


ABSTRACT
Self-adapting software adapts its behavior in an autonomic way, by dynamically adding, suppressing and recomposing components, and by the use of computational reflection. One way to enforce software robustness while adding adaptative behavior is disposing of a formal support allowing these programs to be modeled, and their properties specified and verified. We propose FracL, a formal framework for specifying and reasoning about dynamic reconfiguration programs being written in a Fractal-like programming style. FracL is founded on first order logic, and allows the specification and proof of properties concerning either functional concerns or control concerns. Its encoding using the Focal proof framework, enabled us to prove FracL coherence and to obtain a mechanized framework for reasoning on concrete architectures.


AUTEUR(S)
Marianne SIMONOT, Maria-Virginia APONTE

MOTS-CLÉS
composants, reconfiguration dynamique, Fractal, méthodes formelles.

KEYWORDS
components, dynamic reconfiguration, Fractal, formal methods.

CITATIONS
objet.revuesonline.com/revues/28/citation/12713.html

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 34.95 €
• Non abonné : 34.95 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (454 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier