University Sétif 1 FERHAT ABBAS Faculty of Sciences
Détail de l'auteur
Auteur Boukhers, Ibtissem |
Documents disponibles écrits par cet auteur
Ajouter le résultat dans votre panier Affiner la recherche
Titre : Model-checking de modèles hiérarchiques Type de document : texte imprimé Auteurs : Boukhers, Ibtissem, Auteur ; Bouamari,Abdelkader, Directeur de thèse Editeur : Setif:UFA Année de publication : 2019 Importance : 1 vol (61 f .) Format : 29 cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : Vérification formelle
Model-Checking hiérarchiqueIndex. décimale : 004 - Informatique Résumé : La technique d’analyse de modèles par Model-Checking s'applique souvent sur des modèles de machines d'états aplatis (non-hiérarchiques), et ne propose aucun support pour des modèles hiérarchiques tels que les statecharts et les machines d'états UML. 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 ‘’Flattening Hierarchical Model-Checker’’ développée. Note de contenu :
Sommaire
Keywords .................................................................................................................. i
Résumé ........................................................................................................................... i
Introduction générale .................................................................................................. 1
I.1 Introduction ............................................................................................................ 3
I.2 Model-Checking ...................................................................................................... 3
I.3 Principes du Model-Checking ............................................................................... 3
I.4 Modélisation du comportement ............................................................................ 4
4.1. Système d’automate ....................................................................................... 4
4.2. Structure de Kripke ...................................................................................... 5
I.5 Spécification des propriétés .......................................................................6
5.1. Logique temporelle linéaire .............................................................................. 6
5.2. Logique temporelle arborescente ..................................................................... 7
I.6 Vérification .............................................................................................................. 9
6.1. Model-Checking de LTL .................................................................................. 9
6.2. Model-Checking de CTL ................................................................................. 9
I.7 Model-Cheking symbolique ................................................................................. 11
I.8 Conclusion ............................................................................................................. 12
II.1 Introduction ......................................................................................................... 13
II.2 Motivation ............................................................................................................ 13
II.3 Modèle Statecharts ........................................................................... 1
3.1. Sémantique des Statecharts ............................................................................ 15
II.4 Défis du Model-checking en présence de la hiérarchie ................................... 16
II.5 Travaux connexes ....................................................................... 1
5.1. Technique sans aplatissement ........................................................................ 18
5.2. Techniques avec aplatissement ...................................................................... 23
5.2.1 Model-Checking de Statechart transformé en SMV : ............................... 24
5.2.2 Model-Checking des Statecharts traduit en SPIN: .................................... 31
5.2.3 Environnement de verification des STATEMENT .................................... 35
5.2.4 Vérification des Statecharts avec ESTEREL .............................................. 36
5.2.5 Vérification des State machines réactifs et communicants ........................ 36
5.2.6 Exploitation de la hiérarchie comportementale pour une vérification efficace par Model........................................................................................ 37
II.6 Comparaison des techniques .............................................................................. 38
II.7 Conclusion ........................................................................................................... 39
III.1 Introduction ....................................................................................................... 40
III.2 Déscription formelle ......................................................................... 4
2.1. Déscription générale du système ................................................................ 40
2.2. Structure de kripke hiérarchique .............................................................. 42
III.3 Algorithme d’aplatissement ............................................................................. 43
III.4 Struture de Kripke aplatie ............................................................................... 45
III.5 Conclusion .......................................................................................................... 46
IV.1 Introduction ....................................................................................................... 47
IV.2 Cahier de charges .................................................................................... 4
2.1. Objectifs .......................................................................................................... 47
2.2. Spécification des besoins ................................................................................. 47
2.3. Déscription générale ........................................................................................ 49
IV.3 Analyse et conception ........................................................................................ 49
3.1. Diagramme de cas d’utilisation ...................................................................... 49
3.2. Diagramme de classe ....................................................................................... 50
3.3. Diagramme de séquence ................................................................................. 51
3.4. Diagramme d’activité ...................................................................................... 53
IV.4 Conclusion .......................................................................................................... 54
V.1 Introduction ......................................................................................................... 55
V.2 Environnement ....................................................................................................
2.1. Choix de java................................................................................................ 55
Choix de Eclipse......................................................................
55 2.4.
Démarche......................................................................................................
56 V.3 Implementation de la solution proposée
56 V.4 Évaluation des résultats
......................................................................................
Conclusion............................................................................................
61 Conclusion générale
...................................................................................................
62 Références Bibliographiques.....................................................................................
64 2.3 Choix du XML....................................................................................Côte titre : MAI/0338 En ligne : https://drive.google.com/file/d/1qw6I7KClZ73S94mEwXwolSP44nuGQpyE/view?usp=shari [...] Format de la ressource électronique : Model-checking de modèles hiérarchiques [texte imprimé] / Boukhers, Ibtissem, Auteur ; Bouamari,Abdelkader, Directeur de thèse . - [S.l.] : Setif:UFA, 2019 . - 1 vol (61 f .) ; 29 cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : Vérification formelle
Model-Checking hiérarchiqueIndex. décimale : 004 - Informatique Résumé : La technique d’analyse de modèles par Model-Checking s'applique souvent sur des modèles de machines d'états aplatis (non-hiérarchiques), et ne propose aucun support pour des modèles hiérarchiques tels que les statecharts et les machines d'états UML. 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 ‘’Flattening Hierarchical Model-Checker’’ développée. Note de contenu :
Sommaire
Keywords .................................................................................................................. i
Résumé ........................................................................................................................... i
Introduction générale .................................................................................................. 1
I.1 Introduction ............................................................................................................ 3
I.2 Model-Checking ...................................................................................................... 3
I.3 Principes du Model-Checking ............................................................................... 3
I.4 Modélisation du comportement ............................................................................ 4
4.1. Système d’automate ....................................................................................... 4
4.2. Structure de Kripke ...................................................................................... 5
I.5 Spécification des propriétés .......................................................................6
5.1. Logique temporelle linéaire .............................................................................. 6
5.2. Logique temporelle arborescente ..................................................................... 7
I.6 Vérification .............................................................................................................. 9
6.1. Model-Checking de LTL .................................................................................. 9
6.2. Model-Checking de CTL ................................................................................. 9
I.7 Model-Cheking symbolique ................................................................................. 11
I.8 Conclusion ............................................................................................................. 12
II.1 Introduction ......................................................................................................... 13
II.2 Motivation ............................................................................................................ 13
II.3 Modèle Statecharts ........................................................................... 1
3.1. Sémantique des Statecharts ............................................................................ 15
II.4 Défis du Model-checking en présence de la hiérarchie ................................... 16
II.5 Travaux connexes ....................................................................... 1
5.1. Technique sans aplatissement ........................................................................ 18
5.2. Techniques avec aplatissement ...................................................................... 23
5.2.1 Model-Checking de Statechart transformé en SMV : ............................... 24
5.2.2 Model-Checking des Statecharts traduit en SPIN: .................................... 31
5.2.3 Environnement de verification des STATEMENT .................................... 35
5.2.4 Vérification des Statecharts avec ESTEREL .............................................. 36
5.2.5 Vérification des State machines réactifs et communicants ........................ 36
5.2.6 Exploitation de la hiérarchie comportementale pour une vérification efficace par Model........................................................................................ 37
II.6 Comparaison des techniques .............................................................................. 38
II.7 Conclusion ........................................................................................................... 39
III.1 Introduction ....................................................................................................... 40
III.2 Déscription formelle ......................................................................... 4
2.1. Déscription générale du système ................................................................ 40
2.2. Structure de kripke hiérarchique .............................................................. 42
III.3 Algorithme d’aplatissement ............................................................................. 43
III.4 Struture de Kripke aplatie ............................................................................... 45
III.5 Conclusion .......................................................................................................... 46
IV.1 Introduction ....................................................................................................... 47
IV.2 Cahier de charges .................................................................................... 4
2.1. Objectifs .......................................................................................................... 47
2.2. Spécification des besoins ................................................................................. 47
2.3. Déscription générale ........................................................................................ 49
IV.3 Analyse et conception ........................................................................................ 49
3.1. Diagramme de cas d’utilisation ...................................................................... 49
3.2. Diagramme de classe ....................................................................................... 50
3.3. Diagramme de séquence ................................................................................. 51
3.4. Diagramme d’activité ...................................................................................... 53
IV.4 Conclusion .......................................................................................................... 54
V.1 Introduction ......................................................................................................... 55
V.2 Environnement ....................................................................................................
2.1. Choix de java................................................................................................ 55
Choix de Eclipse......................................................................
55 2.4.
Démarche......................................................................................................
56 V.3 Implementation de la solution proposée
56 V.4 Évaluation des résultats
......................................................................................
Conclusion............................................................................................
61 Conclusion générale
...................................................................................................
62 Références Bibliographiques.....................................................................................
64 2.3 Choix du XML....................................................................................Côte titre : MAI/0338 En ligne : https://drive.google.com/file/d/1qw6I7KClZ73S94mEwXwolSP44nuGQpyE/view?usp=shari [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0338 MAI/0338 Mémoire Bibliothéque des sciences Français Disponible
Disponible