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

Saadi, Wafa (2009) Un cadre formel pour la vérification des modèles UML. Masters thesis, Université Mohamed Khider Biskra.

Preview

Text Inf_m3_2009.pdf Download (135kB) | Preview

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

Actions (login required)

View Item