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 aplatissement
Index. 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 …………………………….………………………………………………………………………71
Côte titre :	MAI/0093
En ligne :	https://drive.google.com/file/d/1qiOdpGGRHRql7oYxqSk65FsZDhTBTT9m/view?usp=shari [...]
Format de la ressource électronique :	pdf

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 aplatissement
Index. 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 …………………………….………………………………………………………………………71
Côte titre :	MAI/0093
En ligne :	https://drive.google.com/file/d/1qiOdpGGRHRql7oYxqSk65FsZDhTBTT9m/view?usp=shari [...]
Format de la ressource électronique :	pdf