ThesesMHK
Le titre de la thèse :
Modélisation des applications distribuées à architecture dynamique : Conception et Validation
Le nom de l'auteur :
Mohamed HADJ KACEM
L'organisme où le doctorant est inscrit :
Université Paul Sabatier, Toulouse III, en cotutelle avec l’Université de Sfax en Tunisie.
La date, l'heure et le lieu de soutenance :
Le 13 Novembre 2008 à 14h30, LAAS-CNRS
La composition du jury :
- M. Rafik Bouaziz, Professeur à la FSEG-Sfax, Tunisie, Rapporteur
- M. Flavio Oquendo, Professeur à l’Université de Bretagne-Sud, Rapporteur
- Me. Brigitte Pradin-Chezalviel, Professeur à Université Paul Sabatier, Toulouse III, Examinateur
- Me. Michelle Sibilla, Professeur à l’Université Paul Sabatier, Toulouse III, Examinateur
- M. Ahmed Hadj-Kacem, Professeur à la FSEG-Sfax, Tunisie, Invité
- M. Mohamed Jmaiel, Professeur à l’ENIS, Sfax, Tunisie, Directeur de thèse Université de Sfax
- M. Khalil Drira, Chargé de recherche au LAAS-CNRS, Directeur de thèse Université de Toulouse III
Le résumé en français :
Nos travaux de recherche consistent à apporter des solutions de modélisation conformément à l'approche MDA proposée par l'OMG. Nos recherches consistent à fournir des solutions permettant de guider et d'assister les activités de modélisation des architectures logicielles. Il s'agit principalement de proposer une démarche de conception orientée modèle permettant de décrire l'architecture logicielle en tenant compte de trois aspects : le style architectural, les opérations de reconfiguration et le protocole de reconfiguration. Nous proposons des notations visuelles permettant de décrire de façon compatible avec UML2.0 l'architecture logicielle. La technique de description que nous adoptons est orientée règles, basée sur les théories de transformation de graphe, permettant, ainsi, de décrire la dynamique structurelle sous forme d'opérations de reconfiguration. Nous avons proposé aussi une technique permettant de décrire le protocole de reconfiguration entre les différentes opérations de reconfiguration. Nous proposons une extension de UML2.0 par un nouveau profil formé de trois méta-modèles. Le premier étend le diagramme de composants et permet de décrire les éléments de base de l'architecture et les connexions qui les associent (méta-modèle style architectural). Le deuxième étend le premier et permet de décrire les opérations de reconfiguration de l'architecture en termes d'ajout et/ou de suppression de composants et/ou de connexions (méta-modèle opération de reconfiguration). Le troisième étend le diagramme d'activité et permet de décrire le protocole de reconfiguration entre les différentes opérations de reconfiguration (méta-modèle protocole de reconfiguration). Nous proposons aussi une approche de validation basée sur des règles intra-modèle et des règles inter-modèles. Les règles intra-modèle permettent de vérifier la cohérence d'un modèle par rapport à son méta-modèle et les règles inter-modèles permettent d'assister le passage d'un modèle à un autre. Nous adoptons également une approche de vérification. Cette approche permet, dans une première étape, une transformation automatique du style architectural et de chaque opération de reconfiguration vers le langage Z. Elle permet dans une deuxième étape, de vérifier la consistance du style architectural et la conformité de l'évolution d'une architecture vis-à-vis de son style architectural. Nous utilisons le système de preuve Z/EVES. Finalement, nous proposons une démarche de modélisation des architectures logicielles dynamiques, appelée X, permettant de décrire les différentes étapes pour modéliser l'architecture logicielle. Elle propose des règles de passage d'un modèle à un autre, elle automatise le processus de validation et assiste l'utilisateur pour vérifier des propriétés architecturales. La démarche proposée est inspirée de la méthode MDA (Model Driven Architecture) et 2TUP (2 Tracks Unified Process) du processus UP (Unified Process). Le profil et la démarche X que nous avons proposés ont fait l'objet d'une implémentation et d'une intégration, sous forme de plug-in java, dans l'atelier d'aide à la conception FUJABA.
Le résumé en anglais :
The Adaptability of network software systems is necessary to guarantee the continuity of services under changing infrastructure constraints and evolving user requirements. The architectural and the behavioural dynamic reconfigurations constitute the two acting categories allowing adaptability of such software systems to be managed. In this paper, we propose to support the architectural reconfiguration-based adaptation and we propose a UML-based approach for describing, validating and checking dynamic software architectures. We introduce a new UML profile associated with three meta-models that we define in order to describe (i) different architectural styles, (ii) their dynamic instances together with the associated reconfiguration operations, and (iii) their reconfiguration protocol. Our approach supports describing the architectural constraints that should be preserved during architecture evolving. The proposed approach supports automatic validation through a set of rules we define and implement for ensuring the correctness of the models w.r.t. the meta-models. These models are automatically transformed into Z specifications. This allows designers to prove, by elaborating Z theorems, the consistency of the defined architectural styles and the conformity of the associated instances and their transformation rules. We define the X Design Process allowing guiding and assisting the architects to model the dynamic software architectures. The X Design Process is partially based on the MDA approach (Model Driven Architecture) and 2TUP Process (2 tracks Unified Process). It is based on two parts: a PIM part and a PSM part. The first models software architecture without worrying about subjacent technologies. The second models their transformation to platform specific models for a given technological platform (Java/EJB, C#, .Net, etc.). The Design Process that we propose uses an iterative and incremental development approach. A software environment supporting the different features of this approach has been developed and integrated as a plugin in the opensource FUJABA tool.
Les mots-clés en français :
Adaptabilité architecturale, Profil UML, Modélisation de l’architecture logicielle, l’architecture dynamique, validation, transformation et vérification formelle.
Les mots-clés en anglais :
Software adaptability, UML Profile, Software architecture modeling, dynamic architecture, validation, formal and checking transformation.