L'environnement FoCaLiZe au service d'UML/OCL

UML et OCL sont des standards pour la modelisation des systemes informatiques et la specication de leurs proprietes. Ils sont largement exploites dans les ateliers de genie logiciel parallelement avec des techniques MDE (Model Driven Engineering) pour la generation systematique du code executable. Cependant, le reproche qui peut etre fait a UML reside dans l'absence de bases permettant l'application des techniques de verications formelles. De meme, le langage OCL, bien que permettant une description formelle des proprietes d'un modele UML, ne dispose pas d'outils pour la verication et la preuve de ses proprietes. C'est pourquoi des methodes formelles ont largement ete utilisees pour la formalisation, l'analyse et la verication des modeles UML/OCL, mais en raison de l'ecart important entre UML et les methodes formelles utilisees, plusieurs fonctionnalites UML/OCL sont ignorees, notamment l'heritage multiple, la derivation des classes liees a partir des classes parametrees et la propagation des contraintes OCL a travers ces fonctionnalites. Dans ce travail de these, nous proposons une formalisation des modeles UML/OCL supportant la plupart des fonctionnalites architecturales et conceptuelles d'UML/OCL, en utilisant le langage FoCaLiZe, un environnement de developpement oriente objet et de programmation certiee, utilisant une approche basee preuve. Plus precisement, nous proposons une transformation formelle des modeles UML/OCL composes de diagrammes de classes, de diagrammes d'etats-transitions et de contraintes OCL en specication FoCaLiZe. Comme application directe nous avons pu proposer un framework MDE, integrant UML/OCL, FoCaLiZe et les regles de transformations proposees, et assistant l'utilisateur en cas d'erreur.