Un cadre formel pour la vérification des modèles UML

Abstract

UML est devenu un standard de la modélisation orienté objet, il intègre le paradigme de développement de logiciel moderne en un langage visuel compréhensif et largement accepté. Les analystes des systèmes sont confrontés à des difficultés lors de l’utilisation d’UML dans le processus de conception des systèmes complexes. Puisqu’une conception efficace de tels systèmes rend nécessaire une vérification formelle mathématiquement précise à chaque phase de la modélisation. Pour des buts d’analyse et de vérification plusieurs travaux ont été élaborés dans le contexte de l’intégration du modèle UML avec des modèles formelle ou bien dans le contexte de la transformation de modèle. Les réseaux de Petri font partie de cette catégorie et plus précisément les ECATnets qui possèdes des outils de vérification et de transformation vers des spécifications algébrique. Pour bénéficier de ces derniers on a fait une transformation des diagrammes de séquences vers les ECATnets à l’aide des grammaires de graphe en utilisant l’outil AToM3. Le résultat obtenu est transformé vers des spécifications Maude pour pouvoir les bénéficier de vérification avec l’outil Maude