[SA08] Une approche formelle de la reconfiguration dynamique
Revue Nationale avec comité de lecture :
Journal L'Objet,
vol. 14(4),
pp. 73-102,
2008
Mots clés: composants, reconï¬guration 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 ex-
primer 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 à com-
posants 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é tra-
duit 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.
Commentaires:
note