| Titre : | Développement d’un outil d’aide à la correction de modèles "Cas de machines abstraite B" |
| Auteurs : | Asma ELGAHRI, Auteur ; Amira Mohammedi, Directeur de thèse |
| Type de document : | Monographie imprimée |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2021 |
| Format : | 1 vol. (62 p.) / ill. / 29 cm |
| Langues: | Français |
| Résumé : | La tâche de modélisation est une tâche très difficile et laborieuse qui nécessite beaucoup d’effort. Même si les spécialistes de modélisation ont pas mal des compétences,parfois le modèle résultant reste incorrect.la correction des erreurs détecter est devenue une tâche laborieuse pour les développeurs Dans ce rapport, nous présentons un outil qui permet Réaliser correction semi-automatique de modèle B . Notre solution se base sur travail (Cai el Al,2018) et (Cai el Al,2019) ,Le principe de cette solution , la proposition 02 types de correction pour le problème dans le cas d’état blocage( isolation et révision) l’isolation est de supprimer un état défectueux en modifiant la pré-condition préalable d’une opération précédente,la révision est de corriger un état défectueux en modifiant les post-conditions d’une opération précédente.L’objectif est de développer l’outil pour la langage jave , qui utilisée proB pour la détection des états de blocage et proposer la solutions corrigées la machine abstraite Cet outil aide les développeurs et leur permet de trouver plus facilement la bonne solution à ce problème |
| Sommaire : |
Introduction générale ix
I État de l’art 1 1 Concepts de base 2 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Méthode B . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2.1 Principes généraux de la méthode B . . . . . . . . . . . . . . 5 1.2.2 Les grandes étapes de la méthode B . . . . . . . . . . . . . . 5 1.2.3 Développement formel : . . . . . . . . . . . . . . . . . . . . . 6 1.2.4 Domaines d’application de B . . . . . . . . . . . . . . . . . . . 6 1.3 Cycle de développement de méthode B . . . . . . . . . . . . . . . . . 7 1.4 Fondements mathématiques de la méthode B . . . . . . . . . . . . . 8 1.4.1 la notation de la théorie des ensemble : . . . . . . . . . . . . . 9 1.4.2 Machine abstraite : . . . . . . . . . . . . . . . . . . . . . . . . 15 1.4.3 Langage des substituons généraliser: . . . . . . . . . . . . . . 18 1.5 Obligations de preuve . . . . . . . . . . . . . . . . . . . . . . . . . . 23 1.5.1 Obligations de preuves de l’initialisation . . . . . . . . . . . . 24 1.5.2 Obligations de preuve des opérations . . . . . . . . . . . . . . 24 1.6 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 1.7 Les notions de raffinement et de modularité en B . . . . . . . . . . . 25 1.7.1 Le raffinement . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 1.7.2 La modularité . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1.8 Outils de V & V . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 Travaux Connexes 30 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.2 Localisation des défauts : . . . . . . . . . . . . . . . . . . . . . . . . 31 2.2.1 isolation : . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.2.2 Révision . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.2.3 Un exemple isolation et de révision : . . . . . . . . . . . . . . 34 2.3 Flux de travail interactif . . . . . . . . . . . . . . . . . . . . . . . . . 38 2.3.1 Exemple d’exécution : . . . . . . . . . . . . . . . . . . . . . . 39 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 II Développement d’un outil pour correction d’un modèle B "Cas de machines abstraite B" 42 3 Conception 43 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.2 Spécification et analyse de besoin . . . . . . . . . . . . . . . . . . . . 44 3.3 Conception . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.3.1 Conception globale . . . . . . . . . . . . . . . . . . . . . . . . 44 3.3.2 Conception détaillée . . . . . . . . . . . . . . . . . . . . . . . 46 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4 Implémentation 49 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 4.2 Outils et langages de développement . . . . . . . . . . . . . . . . . . 50 4.2.1 ProB . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 4.2.2 Langage de programmation Java . . . . . . . . . . . . . . . . 50 4.2.3 Éditeur de programmation NetBeans . . . . . . . . . . . . . . 51 4.2.4 Package Swing . . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.2.5 Système de préparation de documents LATEX . . . . . . . . . . 51 4.2.6 Éditeur (TEX Studio) . . . . . . . . . . . . . . . . . . . . . . . 52 4.3 présentation de l’outil . . . . . . . . . . . . . . . . . . . . . . . . . . 52 4.3.1 Fenêtre d’accueil . . . . . . . . . . . . . . . . . . . . . . . . . 53 4.3.2 Fonctionnalités de l’application . . . . . . . . . . . . . . . . . 56 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 Conclusion générale xii Annexe xiii Bibliography xvii |
| Type de document : | Mémoire master |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| MINF/683 | Mémoire master | bibliothèque sciences exactes | Consultable |
