Bonjour à tous, Je vous invite à la soutenance de ma thèse intitulée "Approche de métamodélisation pour la simulation et la vérification de modèle -- Application à l'ingénierie des procédés" réalisée à l'ENSEEIHT dans le laboratoire IRIT. Cette thèse, encadrée par Xavier CRÉGUT et dirigée par Patrick SALLÉ et Bernard COULETTE, sera soutenue publiquement le vendredi 11 juillet à 11h à la salle des thèses de l'ENSEEIHT, devant le jury : Rapporteurs : Jean BÉZIVIN, Professeur, INRIA-ATLAS, Université de Nantes Pierre-Alain MULLER, Professeur, Université de Haute-Alsace. Examinateurs : Antoine BEUGNARD, HDR, ENST de Bretagne François VERNADAT, Professeur, LAAS CNRS, INSAT Bernard COULETTE, Professeur, IRIT, Université de Toulouse Xavier CRÉGUT, Maître de conférences, IRIT, Université de Toulouse Invité : Patrick FARAIL, AIRBUS France Vous êtes également les bienvenus au pot qui aura lieu au premier étage de l'IRIT-ENSEEIHT, rue d'aubuisson à 17h00. Accès : ------- http://combemale.perso.enseeiht.fr/map/ Résumé : -------- L'ingénierie dirigée par les modèles (IDM) a permis plusieurs améliorations significatives dans le développement de systèmes complexes en permettant de se concentrer sur une préoccupation plus abstraite que la programmation classique. Il s'agit d'une forme d'ingénierie générative dans laquelle tout ou partie d'une application est engendrée à partir de modèles. Une des idées phares est d'utiliser autant de langages de modélisation différents (Domain Specific Modeling Languages -- DSML) que les aspects chronologiques ou technologiques du développement le nécessitent. Le défi actuel de la communauté du génie logiciel est de simplifier la définition de nouveaux DSML en fournissant des technologies du métaniveau telles que des générateurs d'éditeurs syntaxiques (textuels ou graphiques), des outils d'exécution, de validation et de vérification (statique et dynamique). Ces outils de validation et de vérification nécessitent d'expliciter, en plus de la syntaxe abstraite, la sémantique d'exécution du DSML. Au regard des travaux existants dans l'IDM et de l'expérience acquise avec les langages de programmation, nous proposons dans cette thèse une taxonomie précise des techniques permettant d'exprimer une sémantique d'exécution pour un DSML. Nous replaçons ensuite ces différentes techniques au sein d'une démarche complète permettant de décrire un DSML et les outils nécessaires à l'exécution, la vérification et la validation des modèles. La démarche que nous proposons offre une architecture rigoureuse et générique de la syntaxe abstraite du DSML pour capturer les informations nécessaires à l'exécution d'un modèle et définir les propriétés temporelles qui doivent être vérifiées. Nous nous appuyons sur cette architecture générique pour expliciter la sémantique de référence (c.-à-d. issue de l'expérience des experts du domaine) et l'implanter. Plus particulièrement, nous étudions les moyens : - d'exprimer et de valider la définition d'une traduction vers un domaine formel dans le but de réutiliser des outils de model-checking et permettre ainsi la vérification formelle et automatique des propriétés exprimées. - de compléter la syntaxe abstraite par le comportement; et profiter d'outils génériques pour pouvoir simuler les modèles construits. Enfin, il est indispensable de valider les différentes sémantiques implantées vis-à-vis de la sémantique de référence. Aussi, nous proposons un cadre formel pour la métamodélisation, transparent pour le concepteur, permettant d'exprimer la sémantique de référence qui servira de base à cette validation. La démarche est illustrée dans cette thèse à travers le domaine des procédés de développement. Après une étude approfondie de cette ingénierie, et plus particulièrement du langage SPEM proposé par l'OMG, nous définissons l'extension xSPEM permettant de construire des modèles exécutables. Nous décrivons également les outils permettant la vérification formelle et la simulation des modèles xSPEM. La démarche proposée est toutefois générique et a donné lieu à des transferts technologiques dans le projet topcased en établissant des fonctionnalités de vérification et de simulation pour différents langages de l'atelier. -- Benoît COMBEMALE PhD Candidate in Computer Science -- IRIT Laboratory INPT-ENSEEIHT -- Département Télécom & Réseaux 2, rue Charles Camichel, BP 7122 - F 31071 Toulouse Cedex 7 Tel : (+33/0)5 61 58 80 37 Fax : (+33/0)5 61 58 83 06 Mél : benoit.combemale@enseeiht.fr Web : http://combemale.perso.enseeiht.fr