Institution-based Semantics and Tool Support for the UML

Sémantique et outils institutionnels pour le UML Les techniques basées sur des modèles, en particulier le Unified Modeling Language (UML), ont trouvé une large adoption dans l’industrie du logiciel. Les méthodes formelles peuvent produire des logiciels avec des garanties de certaines propriétés souhaitées, ce qui est particulièrement intéressant concernant des questions de sûreté ou de sécurité. Les méthodes formelles ont été utilisées avec beaucoup de succès dans certains domaines comme la programmation des systèmes ferroviaires (ex. la vérification des lignes automatiques du métro parisien). Malgré ces avantages, l’adoption de méthodes formelles dans la plupart de l’industrie du logiciel a été limitée. Cette thèse fait partie d’une série de travaux visant à faciliter l’adoption de méthodes formelles en permettant une utilisation entièrement formelle d’UML. En poursuivant cet objectif,nous voulons suivre les meilleures pratiques d’ingénierie du logiciel comme le principe de non-répétition et la modularité.À cette fin, nous utilisons la théorie des institutions et le Heterogeneous Toolset (HeTS). La théorie des institutions est une manière systématique et modulaire de mettre en relation de différents formalismes. Le Heterogeneous Toolset est basé sur la théorie des institutions et met enœuvre la réutilisation d’outils à travers différents formalismes. C’est dans ce contexte que nous souhaitons intégrer l’UML, en apportant des sémantiques institutionnels et des implémentations dans HeTS pour les différents sous-langages de l’UML. Traductions entre ces institutions donnent alors une sémantique commune. Des traductions vers d’autres langages établis et implémentés dans HeTS nous permettent d’emprunter leurs outils.Les contributions de cette thèse à l’effort décrit ci-dessus consistent dans le développement de langages pour les UML State Machines et les UML Composite Structures et les traductions de ces langages vers le langage Casl. Nous présentons nos langages et traductions en termes de la théorie des institutions, ainsi qu’une implémentation prototypique dans HeTS. De plus, nous vérifions les propriétés de quelques spécifications dans nos langages pour une démonstration de la faisabilité de notre approche. Les expériences de nos travaux sur l’institutionnalisation, sur la programmation et la vérification font d’ailleurs ressortir plusieurs possibilités de travaux futurs.