Un Cadre Formel Pour La Vérification Des Modèles Uml
Résumé: 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
Mots-clès:
Nos services universitaires et académiques
Thèses-Algérie vous propose ses divers services d’édition: mise en page, révision, correction, traduction, analyse du plagiat, ainsi que la réalisation des supports graphiques et de présentation (Slideshows).
Obtenez dès à présent et en toute facilité votre devis gratuit et une estimation de la durée de réalisation et bénéficiez d'une qualité de travail irréprochable et d'un temps de livraison imbattable!
Aucun fichier associé
Si le fichier est volumineux, l'affichage peut échouer. Vous pouvez obtenir le fichier directement en cliquant sur le bouton "Télécharger".
