THÈSE soutenue en vue de l'obtention du titre de

Jean Bézivin

Description

Niveau: Supérieur, Doctorat, Bac+8
Année : 2008 THÈSE soutenue en vue de l'obtention du titre de DOCTEUR EN INFORMATIQUE DE L'UNIVERSITÉ DE TOULOUSE délivré par l'INSTITUT NATIONAL POLYTECHNIQUE DE TOULOUSE Approche de métamodélisation pour la simulation et la vérification de modèle Application à l'ingénierie des procédés Présentée et soutenue publiquement par BENOÎT COMBEMALE le 11 juillet 2008 à l'ENSEEIHT, devant le jury composé des membres suivants : Rapporteurs : Jean BÉZIVIN Professeur, INRIA-ATLAS, Université de Nantes Pierre-Alain MULLER Professeur, Université de Haute-Alsace Examinateurs : Antoine BEUGNARD (président) Professeur, ENST de Bretagne François VERNADAT Professeur, LAAS CNRS, Université de Toulouse Bernard COULETTE Professeur, IRIT, Université de Toulouse Xavier CRÉGUT (encadrant) Maître de conférences, IRIT, Université de Toulouse Invités : Patrick FARAIL AIRBUS France ÉCOLE DOCTORALE MITT «Mathématiques Informatique et Télécommunications de Toulouse » Directeurs : Patrick SALLÉ (IRIT, ENSEEIHT) et Bernard COULETTE (IRIT, UTM) Laboratoire : Institut de Recherche en Informatique de Toulouse (IRIT, UMR 5505)

• cadre formel pour la métamodélisation


• regard des travaux existants dans l'idm et de l'expérience acquise avec les langages de programmation


• merci


• ticulièrement du langage spem


• ton


• idm


• simulation des modèles xspem


• éternel merci

Sujets

• Institut de recherche en informatique de Toulouse
• Institut national polytechnique de Toulouse
• Müller
• Université de Nantes
• Université de Toulouse
• Upper Alsace University

Informations

• Publié par: profil-feym-2012
• Nombre de lectures: 78
• Langue: Français
• Poids de l'ouvrage: 2 Mo

Extrait

Année:2008
THÈSE
soutenueenvuedel’obtentiondutitrede
DOCTEURENINFORMATIQUE
DEL’UNIVERSITÉDETOULOUSE
délivrépar
l’INSTITUTNATIONALPOLYTECHNIQUEDETOULOUSE
Approchedemétamodélisation
pourlasimulationetlavérificationdemodèle
Applicationàl’ingénieriedesprocédés
Présentéeetsoutenuepubliquementpar
BENOÎT COMBEMALE
le11juillet2008àl’ENSEEIHT,
devantlejurycomposédesmembressuivants:
Rapporteurs: Jean BÉZIVIN
Professeur,INRIA ATLAS,UniversitédeNantes
Pierre Alain M ULLER
Professeur,UniversitédeHaute Alsace
Examinateurs: Antoine BEUGNARD (président)
Professeur,ENSTdeBretagne
François VERNADAT
Professeur,LAASCNRS,UniversitédeToulouse
Bernard COULETTE
Professeur,IRIT,UniversitédeToulouse
Xavier CRÉGUT (encadrant)
Maîtredeconférences,IRIT,UniversitédeToulouse
Invités: Patrick FARAIL
AIRBUSFrance
ÉCOLE DOCTORALE MITT
«MathématiquesInformatiqueetTélécommunicationsdeToulouse»
Directeurs:PatrickSALLÉ(IRIT,ENSEEIHT)etBernardCOULETTE(IRIT,UTM)
Laboratoire:InstitutdeRechercheenInformatiquedeToulouse(IRIT,UMR5505)2Remerciements
La réalisation d’une thèse est certes un long travail mais aussi une aventure
humaine sans laquelle nos recherches auraient peu de sens. C’est celle ci que je
vais essayer de retracer dans ces remerciements. Cette étape importante n’est pas
laplussimple,etjevousprieparavancedem’excuserpourlesoubliséventuels.
Mes remerciements vont tout d’abord à JEAN BÉZIVIN et PIERRE-ALAIN
MULLER pour avoir accepté de relire mon manuscrit et d’en être les rapporteurs.
Je tiens aussi à remercier Jean pour son écoute tout au long de mes travaux et
pournosnombreuxéchangesàl’occasiondeconférences,quiontsuàchaquefois
m’éclairer dans mon travail. Un merci également à Pierre Alain pour sa relecture
minutieusedumanuscrit,sesremarquesenrichissantesetsavisionéclairéepermet
tantdemettreenperspectivesmontravail.
Je remercie aussi les personnes qui ont acceptées d’évaluer mon travail et de
participer à mon jury. ANTOINE BEUGNARD pour avoir présidé le jury et pour
avoir partagé avec moi des discussions très intéressantes. FRANÇOIS VERNADAT
pournoscollaborationstoutaulongdesannées,sadisponibilitéetsaréactivitédans
letravail.PATRICK FARAILpoursadisponibilitéetsescompétencesquiontfaitde
maparticipationauprojet TOPCASED unmomentaussienrichissantqu’agréable.
MerciàPATRICK SALLÉetBERNARD COULETTEpourm’avoirfaitconfiance
toutaulongdecesannéesetpouravoiracceptédedirigercettethèse.Merciégale
ment à MARC PANTEL pour m’avoir permis de m’intégrer dans différents projets
derechercheetdeparticiperàdenombreuxcongrès.
Unéternelmercià XAVIER CRÉGUT.Mercid’abordpourtaconfianceetpour
avoir accepté d’encadrer mon stage de Master Recherche et mes travaux de thèse.
Tonécoute,tonsoutiensanslimiteettonamitiéontfaitdecesannéesdesmoments
inoubliables et si agréables. Par ailleurs, ta disponibilité, ta rigueur et tes conseils
ont fait de cette période une formation à la recherche très enrichissante et l’objet
d’untravailintense.Pourtoutcelajetesuisinfinimentredevable.
Mestravauxsesontnourrisdenombreuxéchangesquiontsubaliserlechemin
demathèse.Fruitsderencontresmultiples,ilsontainsicontribuéàl’aboutissement
de mon travail et à le rendre si agréable et passionnant. Pour cela, je remercie
RÉDA BENDRAOU, MARIE-PIERRE GERVAIS, PIERRE MICHEL et FRANÇOIS
VERNADAT,maiségalementtousceuxavecquij’aieulachanced’échanger.
34
Ce travail a aussi et avant tout été réalisé au sein d’une équipe de recherche
dont les relations entre ses membres sont le moteur au quotidien de mes travaux.
Ainsi,merciàXAVIER THIRIOUXetPIERRE-LOÏC GAROCHEpourlesnombreux
moments et réunions de travail passés ensemble, à chaque fois très agréables. Un
clin d’oeil à Pierre Loïc pour son soutien constant et son amitié égayant au quo
tidien le travail. Merci aussi pour tous ces cafés préparés avec amour. Je remercie
d’autrepartmesco bureau, M ARCEL GANDRIAU et GÉRARD PADIOU,quim’ont
accueilli parmi eux comme un véritable collègue et m’ont toujours offert de leurs
tempsetleursécouteslorsquej’airencontrédesdifficultés.Mercienfinauxautres
collèguespourlesmomentsagréablespassésensemble:NASSIMA,NADÈGE,LES
PHILIPPE(S), SANDRINE, TANGUY,...
Si l’objet de ces remerciements est de retracer l’aventure humaine vécue au
cours de ces trois dernières années, je ne peux oublier DANIEL HAGIMONT pour
notrecollaborationdynamique,amicaleetplaisante.
En qualité de responsable pédagogique et pour son écoute constante au cours
de mes trois années de monitorat, je tiens à remercier MARC BOYER. Je remercie
également CHRISTIAN FRABOUL pour son accueil au sein de l’équipe pédago
giquedesondépartementdel’ENSEEIHT.
Je tiens aussi à souligner la disponibilité, le soutien permanent et la bonne
humeurdenotregrandetmeilleurchefMichelainsiquedessecrétairesexception
nelles,LesSylviesetSabyne.
Pour terminer cette aventure humaine mais néanmoins professionnelle, je ne
peuxoublierl’équipedel’IUTdeBlagnac,avecunmerciparticulieràLAURENCE,
ALAIN et JEAN-MICHEL pour leur soutien constant et leur présence lors de ma
soutenance.
Ces années de travail n’auraient pu être réalisées sans un soutien extérieur et
infini de ma famille et de mes amis. Mes parents d’abord, MARTINE et CHRIS-
TIAN,sanslesquelsjen’auraijamaispuenarriverlà.Mercipourcela,merciaussi
pour votre compréhension et vos sacrifices. Merci aussi à mes soeurs, SANDRINE
et STÉPHANIE, ainsi qu’à leurs petites familles. je leur prie de voir aussi dans ces
quelques lignes mes excuses pour l’éloignement toutes ces dernières années. En
fin,VÉRONIQUE,quiapartagéauquotidienavecmoilesbonscommelesmauvais
moments avec une compréhension saisissante. Elle a su par son amour baliser le
chemindemonbonheuretégayerchaquejourpassépourpréparercettethèse.
MerciauKREUL,monéternelcompagnonderoute,ainsiqu’atoutel’équipede
FASOLIDARITÉ. Merci pour la bonne humeur d’ELSA, de NANOU et de LUCAS.
Merci pour les moments de détente avec toute La bande de Millau ainsi que pour
leursamitiés.DADOU,LUCAT,LUCHIO,PSYKO,PALPABLE,KEBAB,L’ITALIEN,
BOUTCH, LE NAIN, KOALA, PIERROT,LES JO, FANNY et A-G-UEDE,recevezici
toutemonamitié.Etàceuxquejen’oublieraijamais, CARO et YANN.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
concentrersurunepréoccupationplusabstraitequelaprogrammationclassique.Il
s’agitd’uneformed’ingénieriegénérativedanslaquelletoutoupartied’uneappli
cationestengendréeàpartirdemodèles.Unedesidéespharesestd’utiliserautant
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 ou
tilsd’exécution,devalidationetdevérification(statiqueetdynamique).Cesoutils
de validation et de vérification nécessitent d’expliciter, en plus de la syntaxe abs
traite,lasémantiqued’exécutionduDSML.
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écisedestechniquespermettantd’exprimerunesémantiqued’exécutionpourun
DSML.Nousreplaçonsensuitecesdifférentestechniquesauseind’unedémarche
complètepermettantdedécrireunDSMLetlesoutilsnécessairesàl’exécution,la
vérificationetlavalidationdesmodèles.
Ladémarchequenousproposonsoffreunearchitecturerigoureuseetgénérique
delasyntaxeabstraiteduDSMLpourcapturerlesinformationsnécessairesàl’exé
cution d’un modèle et définir les propriétés temporelles qui doivent être vérifiées.
Nousnousappuyonssurcettearchitecturegénériquepourexpliciterlasémantique
de référence (c. à d. issue de l’expérience des experts du domaine) et l’implanter.
Plusparticulièrement,nousétudionslesmoyens:
– d’exprimer et de valider la définition d’une traduction vers un domaine for-
mel dans le but de réutiliser des outils de model checking et permettre ainsi
lavérificationformelleetautomatiquedespropriét