Soutenance de thèse de Julien DORMOY le 16/12/2011 à 10 h - Salle des Actes UFR ST

Dans cette thèse, nous nous intéressons aux systèmes à composants dont les architectures évoluent dans le temps en fonction des ressources disponibles et des besoins d'adaptation à l'environnement. Pour ces systèmes, les reconfigurations dynamiques sont utilisées pour répondre aux besoins d'adaptation et ainsi améliorer leur disponibilité et leur fiabilité. L'étude des reconfigurations dynamiques des systèmes ainsi que des mécanismes d'adaptation sont des domaines de recherche actifs motivés par des applications pratiques. Dans ce cadre, notre objectif principal est de définir un cadre formel nous permettant de spécifier et vérifier les reconfigurations dynamiques de systèmes à composants.

Pour répondre à cet objectif général, cette thèse propose un formalisme permettant de modéliser les systèmes à composants supportant les reconfigurations dynamiques dont nous nous assurons de la cohérence. Dans le but faciliter le développement de ces systèmes, nous étudions le raffinement de ce modèle. Nous définissons aussi des politiques d'adaptation permettant de gérer l'exécution des reconfigurations dynamiques en fonction de l'environnement du système.

Dans le but de répondre au besoin de spécification du comportement souhaité d'un système à composants reconfigurable, nous définissons une logique permettant de spécifier des contraintes architecturales et temporelles. Nous proposons une démarche permettant de vérifier ces contraintes, d'une part, d'une façon statique grâce à la combinaison de techniques de preuve et de model-checking et, d'autre part, de façon dynamique en utilisant des techniques de vérification à l'exécution de ces propriétés sur les modèles à composants. Pour ce dernier aspect, nous proposons une variante de la logique temporelle adaptée pour être utilisée dans un cadre de vérification à l'exécution. Nous utilisons l'évaluation des propriétés lors de l'exécution pour guider les reconfigurations dynamiques des modèles à composants dans le but d'éviter la violation des propriétés. 

Les contributions de cette thèse ont été expérimentées sur la plateforme Fractal qui offre un modèle supportant les reconfigurations dynamiques. Nous illustrons les différentes démarches proposées grâce au développement des prototypes dans cette plateforme.

Mots clés : Composants, Adaptation, Reconfiguration, Raffinement, Propriétés temporelles.