University Sétif 1 FERHAT ABBAS Faculty of Sciences
Détail de l'auteur
Auteur LAMRI SAHRAOUI, Ahlem |
Documents disponibles écrits par cet auteur
Ajouter le résultat dans votre panier Affiner la recherche
Titre : Model-Checking hiérarchique Type de document : texte imprimé Auteurs : LAMRI SAHRAOUI, Ahlem ; BOUAMARI,A, Directeur de thèse Editeur : Setif:UFA Année de publication : 2016 Importance : 1 vol (72f.) Format : 29 cm Langues : Anglais (eng) Catégories : Thèses & Mémoires:Informatique Mots-clés : Génie Logiciel
vérification formelle
Model-Checking hiérarchique
modélisation du système
structure de Kripke
machine d’état
automate
état-transition
aplatissementIndex. décimale : 004 Informatique Résumé : Résumé
La vérification des systèmes hiérarchiques par Model-Checking est souvent difficile et
nécessite une adaptation des structures ou des algorithmes traditionnels. Ce mémoire propose
une solution basée sur l'aplatissement pour analyser formellement des modèles hiérarchiques
formalisés avec des structures de Kripke. Il décrit dans ce contexte la conception détaillée et
l'implémentation de la solution logicielle HKS-Checker développée.
Note de contenu : Table de matières
Résumé ………………………………………………………………………..……………………….i
Remerciements ………………………………………………………………………………………ii
Dédicace ……………………………………………………………………………………………...iii
Table de matières …………………………………………………………………………………...iv
Introduction général ......................................................................................................... 1
Chapitre 1 Model-Checking
1.1 Introduction ............................................................................................................ 4
1.2 Vérification formelle ....................................................................................................... 4
1.3 Model-Checking ............................................................................................................. 5
1.3.1 Principe de Model-Checking ............................................................................................. 5
1.3.2 Outils du Model-Checking................................................................................................. 5
1.3.3 Problèmes du Model-Checking ......................................................................................... 6
1.4 Model-Checking symbolique....................................................................................................... 6
1.4.1 Diagrammes de décision binaire ...................................................................................... 6
1.4.2 Représentation graphique................................................................................................. 7
1.5 La modélisation du système ........................................................................................................ 7
1.5.1 Automate ............................................................................................................................ 8
1.5.2 Structures de Kripke......................................................................................................... 9
1.5.3 Le modèle de Statechart................................................................................................... 10
1.6 Conclusion............................................................................................................... 11
Chapitre 2 Model-Checking de modèles hiérarchique
2.1 Introduction .............................................................................................................. 12
2.2 Le processus de revue systématique.......................................................................................... 12
2.3 Travaux connexes............................................................................................................ 15
2.3.1 Technique sans aplatissement ........................................................................................ 15
Analyse explicite .................................................................................................................. 15
Analyse symbolique............................................................................................................. 20
2.3.2 Technique avec aplatissement ........................................................................................ 21
2.4 Comparaisons des solutions ...................................................................................................... 28
2.5 Appréciations des travaux ......................................................................................................... 29
2.6 Conclusion......................................................................................................................... 30
Chapitre 3 'Hierarchical Model-Checker' Contribution
3.1 Introduction ................................................................................................................ 31
3.2 Description formelle........................................................................................................ 32
3.3 Structure de Kripke hiérarchique............................................................................................. 34
3.4 Aplatissement ........................................................................................................... 35
3.5 Structure de Kripke aplatie................................................................................................. 36
3.6 Conclusion.......................................................................................................... 37
Chapitre 4 'HKS-Checker' Analyse et conception
4.1 Introduction ........................................................................................................... 38
4.2 Cahier de charges ..............................................................................................39
4.2.1 Objectifs ......................................................................................................... 39
4.2.2 Spécification des besoins........................................................................................ 39
Besoins fonctionnels ................................................................................................. 39
Besoins non fonctionnels et choix techniques.................................................................... 41
4.2.3 Description générale................................................................................................ 41
4.3 Analyse................................................................................................................ 42
4.3.1 Diagramme de cas d’utilisation...................................................................................... 42
4.3.2 Description détaillée de diagramme de cas d’utilisation.............................................. 42
4.3.3 Diagramme de classes de données.................................................................................. 47
4.3.4 Diagramme de classes de dialogue ................................................................................. 48
4.4 Conception............................................................................................................. 48
4.4.1 Diagramme de classes participantes...................................................................................... 48
4.4.2 Diagrammes de séquence ...................................................................................................... 50
4.4.3 Diagrammes d’activités.................................................................................................... 54
4.5 Conclusion................................................................................................................... 56
Chapitre 5 'HKS-Checker' Implémentation
5.1 Introduction ............................................................................................................... 57
5.2 Environnement ............................................................................................................. 58
5.2.1 Choix de java ........................................................................................................... 58
5.2.2 Choix d’éclipse......................................................................................................... 58
5.2.3 Démarche ............................................................................................................... 58
5.3 Implémentation de la solution proposée.................................................................................... 59
5.4 Evaluations des résultats................................................................................................ 59
5.5 Conclusion................................................................................................................ 67
Conclusion général ……………………………………………………………………………………………………………………..68
Références Bibliographiques …………………………….………………………………………………………………………71Côte titre : MAI/0093 En ligne : https://drive.google.com/file/d/1qiOdpGGRHRql7oYxqSk65FsZDhTBTT9m/view?usp=shari [...] Format de la ressource électronique : Model-Checking hiérarchique [texte imprimé] / LAMRI SAHRAOUI, Ahlem ; BOUAMARI,A, Directeur de thèse . - [S.l.] : Setif:UFA, 2016 . - 1 vol (72f.) ; 29 cm.
Langues : Anglais (eng)
Catégories : Thèses & Mémoires:Informatique Mots-clés : Génie Logiciel
vérification formelle
Model-Checking hiérarchique
modélisation du système
structure de Kripke
machine d’état
automate
état-transition
aplatissementIndex. décimale : 004 Informatique Résumé : Résumé
La vérification des systèmes hiérarchiques par Model-Checking est souvent difficile et
nécessite une adaptation des structures ou des algorithmes traditionnels. Ce mémoire propose
une solution basée sur l'aplatissement pour analyser formellement des modèles hiérarchiques
formalisés avec des structures de Kripke. Il décrit dans ce contexte la conception détaillée et
l'implémentation de la solution logicielle HKS-Checker développée.
Note de contenu : Table de matières
Résumé ………………………………………………………………………..……………………….i
Remerciements ………………………………………………………………………………………ii
Dédicace ……………………………………………………………………………………………...iii
Table de matières …………………………………………………………………………………...iv
Introduction général ......................................................................................................... 1
Chapitre 1 Model-Checking
1.1 Introduction ............................................................................................................ 4
1.2 Vérification formelle ....................................................................................................... 4
1.3 Model-Checking ............................................................................................................. 5
1.3.1 Principe de Model-Checking ............................................................................................. 5
1.3.2 Outils du Model-Checking................................................................................................. 5
1.3.3 Problèmes du Model-Checking ......................................................................................... 6
1.4 Model-Checking symbolique....................................................................................................... 6
1.4.1 Diagrammes de décision binaire ...................................................................................... 6
1.4.2 Représentation graphique................................................................................................. 7
1.5 La modélisation du système ........................................................................................................ 7
1.5.1 Automate ............................................................................................................................ 8
1.5.2 Structures de Kripke......................................................................................................... 9
1.5.3 Le modèle de Statechart................................................................................................... 10
1.6 Conclusion............................................................................................................... 11
Chapitre 2 Model-Checking de modèles hiérarchique
2.1 Introduction .............................................................................................................. 12
2.2 Le processus de revue systématique.......................................................................................... 12
2.3 Travaux connexes............................................................................................................ 15
2.3.1 Technique sans aplatissement ........................................................................................ 15
Analyse explicite .................................................................................................................. 15
Analyse symbolique............................................................................................................. 20
2.3.2 Technique avec aplatissement ........................................................................................ 21
2.4 Comparaisons des solutions ...................................................................................................... 28
2.5 Appréciations des travaux ......................................................................................................... 29
2.6 Conclusion......................................................................................................................... 30
Chapitre 3 'Hierarchical Model-Checker' Contribution
3.1 Introduction ................................................................................................................ 31
3.2 Description formelle........................................................................................................ 32
3.3 Structure de Kripke hiérarchique............................................................................................. 34
3.4 Aplatissement ........................................................................................................... 35
3.5 Structure de Kripke aplatie................................................................................................. 36
3.6 Conclusion.......................................................................................................... 37
Chapitre 4 'HKS-Checker' Analyse et conception
4.1 Introduction ........................................................................................................... 38
4.2 Cahier de charges ..............................................................................................39
4.2.1 Objectifs ......................................................................................................... 39
4.2.2 Spécification des besoins........................................................................................ 39
Besoins fonctionnels ................................................................................................. 39
Besoins non fonctionnels et choix techniques.................................................................... 41
4.2.3 Description générale................................................................................................ 41
4.3 Analyse................................................................................................................ 42
4.3.1 Diagramme de cas d’utilisation...................................................................................... 42
4.3.2 Description détaillée de diagramme de cas d’utilisation.............................................. 42
4.3.3 Diagramme de classes de données.................................................................................. 47
4.3.4 Diagramme de classes de dialogue ................................................................................. 48
4.4 Conception............................................................................................................. 48
4.4.1 Diagramme de classes participantes...................................................................................... 48
4.4.2 Diagrammes de séquence ...................................................................................................... 50
4.4.3 Diagrammes d’activités.................................................................................................... 54
4.5 Conclusion................................................................................................................... 56
Chapitre 5 'HKS-Checker' Implémentation
5.1 Introduction ............................................................................................................... 57
5.2 Environnement ............................................................................................................. 58
5.2.1 Choix de java ........................................................................................................... 58
5.2.2 Choix d’éclipse......................................................................................................... 58
5.2.3 Démarche ............................................................................................................... 58
5.3 Implémentation de la solution proposée.................................................................................... 59
5.4 Evaluations des résultats................................................................................................ 59
5.5 Conclusion................................................................................................................ 67
Conclusion général ……………………………………………………………………………………………………………………..68
Références Bibliographiques …………………………….………………………………………………………………………71Côte titre : MAI/0093 En ligne : https://drive.google.com/file/d/1qiOdpGGRHRql7oYxqSk65FsZDhTBTT9m/view?usp=shari [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0093 MAI/0093 Mémoire Bibliothéque des sciences Anglais Disponible
Disponible