| Titre : | un cadre formel pour la vérification des modèles UML |
| Auteurs : | Wafa Saadi, Auteur ; Allaoua Chaoui, Directeur de thèse |
| Type de document : | Mémoire magistere |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2009 |
| ISBN/ISSN/EAN : | TINF/15 |
| Format : | 1 vol. (81 p.) / 30 cm |
| Langues: | Français |
| 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. |
| Sommaire : |
Introduction générale 1 Chapitre1 : La modélisation UML 1.1. Introduction 5 1.2. La modélisation 6 1.2.a.Qu’est ce qu’un modèle 6 1.2.b.Pourquoi modéliser 6 1.2.c.Les quatre principes de la modélisation 7 1.2.d.La modélisation Orientée Objet 8 1.3. Introduction a UML 9 1.3.a.UML est un langage de modélisation 9 1.3.b.Historique d’UML 10 1.3.c.La méthodologie UML 11 1.4. La notation UML 12 1.4.a.Les éléments d’UML 13 1.4.b.Les relations dans UML 15 1.4.c.Les diagrammmes 16 1.5. Les diagrammes UML 16 1.5.a.Les diagrammes structurels 17 1.5.b.Les diagrammes comportementaux 20 1.6 Le métamodèle UML 22 1.7 Conclusion 24 Chapitre 2 : transformations des modèles 2.1. Introduction 26 2.2. Principe du MDA 27 2.3. Architecture MDA 28 2.4. Les différents modèles du MDA 28 2.4.a.Qu’est ce qu’une plateforme 28 2.4.b.CIM (Computation Independent Model) 29 2.4.c.PIM (Platform Independent Model) 29 2.4.d.PSM (Platform Specific Model) 29 2.5. La transformation des modèles 30 2.6. La méta-modélisation et la transformation 30 2.7. Classification des approches de transformations 33 2.7.a.Transformations de type Modèle vers code 34 2.7.b.Transformations de type modèle vers modèle 34 2.8. Transformation de graphes 37 2.8.a.Graphes non orientés 38 2.8.b.Graphes orientés 38 2.8.c.Les relations entre les graphes 39 2.8.d. Le principe de règles 40 2.8.e. Application des règles 40 2.9. Conclusion 41 Chapitre 3 : Les réseaux de Petri 3.1 Introduction 42 3.2 Qu’est ce que les réseaux de Petri? 42 3.2.a. L'aspect structurel 43 3.2.b. L’aspect comportemental 43 3.2.c. Représentation d'un réseau de Petri 45 3.3 Les réseaux de Petri colorés 47 3.4 Les réseaux de Petri à Objet 48 3.5 Les réseaux de Petri temporisés 48 3.6 Les réseaux de Petri temporels 50 3.7 Les réseaux de Petri stochastiques 50 3.8 Les ECATNets 51 3.9 Conclusion 52 Chapitre 4 : transformation des modèles UML vers les RDP 4.1. Introduction 53 Partie1 : Cadre général des transformations de modèle UML 4.2.1. UML et la vérification 54 4.2.2. UML et la transformation de modèles 55 4.2.3. Transformation des modèles UML vers les réseaux de Petri 55 4.2.3.a. Réseaux de Petri colorés 55 4.2.3.b. Réseaux de Petri Stochastiques 56 4.2.3.c. Réseaux de Petri Orientés objet 56 4.2.3.d. Réseaux de Petri temporisé 57 4.2.4. UML et la transformation de graphes 57 4.2.5. Transformation des diagrammes de séquence vers les réseaux de Petri 58 4.2.6. Discussion 59 Partie2 : Une grammaire de graphe pour la transformation du diagramme de séquence vers les ECATNets. 4.3.1. Présentation de l’outil de transformation utilisée : AToM3 60 4.3.2. Méta-modèle du diagramme de séquence 61 4.3.3. Méta-modèle des ECATNets 64 4.3.4. Grammaire de graphe proposée 66 4.3.5. Exemple de transformation d’un diagramme de séquence vers un ECATNet 75 4.4. Conclusion 79 Conclusion générale 80 Bibliographie 82 |
| Type de document : | Thése magister |
| En ligne : | http://thesis.univ-biskra.dz/339/1/Inf_m3_2009.pdf |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| TINF/15 | Mémoire de magister | bibliothèque sciences exactes | Consultable |
