L'environnement FoCaLiZe au service d'UML/OCL

Résumé

UML et OCL sont des standards pour la modélisation des systèmes informatiques et la spécication de leurs propriétés. Ils sont largement exploités dans les ateliers de génie logiciel parallèlement avec des techniques MDE (Model Driven Engineering) pour la génération systématique du code exécutable. Cependant, le reproche qui peut être fait à UML réside dans l'absence de bases permettant l'application des techniques de vérications formelles. De même, le langage OCL, bien que permettant une description formelle des propriétés d'un modèle UML, ne dispose pas d'outils pour la vérication et la preuve de ses propriétés. C'est pourquoi des méthodes formelles ont largement été utilisées pour la formalisation, l'analyse et la vérication des modèles UML/OCL, mais en raison de l'écart important entre UML et les méthodes formelles utilisées, plusieurs fonctionnalités UML/OCL sont ignorées, notamment l'héritage multiple, la dérivation des classes liées à partir des classes paramétrées et la propagation des contraintes OCL à travers ces fonctionnalités. Dans ce travail de thèse, nous proposons une formalisation des modèles UML/OCL supportant la plupart des fonctionnalités architecturales et conceptuelles d'UML/OCL, en utilisant le langage FoCaLiZe, un environnement de développement orienté objet et de programmation certiée, utilisant une approche basée preuve. Plus précisément, nous proposons une transformation formelle des modèles UML/OCL composés de diagrammes de classes, de diagrammes d'états-transitions et de contraintes OCL en spécication FoCaLiZe. Comme application directe nous avons pu proposer un framework MDE, intégrant UML/OCL, FoCaLiZe et les règles de transformations proposées, et assistant l'utilisateur en cas d'erreur.

Citer ce document

Accès au document

Ce document est hébergé sur son dépôt institutionnel d'origine.

Auteur(s)

Statistiques

Consultations : 2

Téléchargements : 0