University Sétif 1 FERHAT ABBAS Faculty of Sciences
Détail de l'auteur
Auteur BOUAMARI,A |
Documents disponibles écrits par cet auteur
Ajouter le résultat dans votre panier Affiner la recherche
Titre : Assistant de spécification de propriétés a base d’ontologie Type de document : texte imprimé Auteurs : MEGUELATI ,Khadidja ; BOUAMARI,A, Directeur de thèse Editeur : Setif:UFA Année de publication : 2016 Importance : 1 vol (91f.) Format : 29 cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : Génie Logiciel
model-cheking
logique temporelle
patterns de spécification
ontologieIndex. décimale : 004 Informatique Résumé : Résumé
La spécification de propriétés à vérifier dans le cadre d’une vérification formelle par
model-checking est souvent difficile et nécessite des compétences spécialisées. Ce mémoire
présente une solution d'assistance basée sur les patterns de spécification et les ontologies et
propose une conception détaillée d’une solution logicielle de spécification assistée de
propriétés CTL. Le mémoire discute également les détails de réalisation de l’outil développé
Property-Specifier et les résultats obtenus.Note de contenu : Table des matières
Introduction générale ............................................................................................... 1
Partie I : Etat de l'art
Chapitre 1 Model-Checking
1.1 Introduction................................................................................................. 3
1.2 Vérification formelle................................................................................... 3
1.3 Model-Checking ........................................................................................... 4
1.3.1 Principes du Model-Checking.............................................................. 4
1.3.2 Outils du Model-Checking ................................................................... 5
1.3.3 Problèmes du Model-Checking............................................................ 5
1.4 Techniques de spécification........................................................................ 5
1.4.1 Logiques propositionnelles.................................................................. 6
1.4.2 Logiques temporelles ........................................................................... 6
1.4.3 Logiques temporelles temporisées...................................................... 6
1.5 Logique temporelle CTL............................................................................ 7
1.5.1 Le choix de CTL................................................................................... 7
1.5.2 Constituants de CTL............................................................................ 7
1.5.3 Classes de propriétés............................................................................ 9
1.5.4 Syntaxe de CTL.................................................................................... 9
1.5.5 Sémantique de CTL ............................................................................. 9
1.6 Conclusion ................................................................................................. 10
Chapitre 2 Spécification Assistée .................................Erreur ! Signet non défini.
2.1 Introduction............................................................................................... 11
2.2 Patterns de spécification........................................................................... 12
2.2.1 Classification des patterns................................................................. 13
2.2.2 Scopes (Portées des patterns)............................................................ 14
2.3 Travaux basés sur les patterns de spécification ..................................... 14
2.3.1 Support du choix des patterns .......................................................... 14
2.3.2 Nouvelles classifications des patterns............................................... 17
2.3.3 Autre assistants................................................................................... 19
2.3.4 Bilan sur l’utilisation des patterns.................................................... 21
2.4 Utilisations des ontologies dans la spécification des exigences ............. 22
2.4.1 Bilan sur l’utilisation des ontologies................................................. 26
2.5 Conclusion ................................................................................................. 27
Chapitre 3 Ontologies............................................................................................. 28
3.1 Introduction............................................................................................... 28
3.2 Apparition des ontologies......................................................................... 29
3.3 Définitions.................................................................................................. 29
3.4 Composants d’une ontologie .................................................................... 30
2.4.1 Concepts.............................................................................................. 30
2.4.2 Relations.............................................................................................. 31
2.4.3 Axiomes et instances .......................................................................... 32
3.5 Dimensions de classification des ontologies............................................ 33
2.5.1 Typologie selon l’objet de conceptualisation ................................... 33
2.5.2 Typologie selon le niveau de détails de l’ontologie.......................... 35
2.5.3 Typologie selon le niveau de complétude ......................................... 36
2.5.4 Typologie selon le niveau du formalisme ......................................... 36
3.6 OWL : le standard du Web sémantique ................................................. 37
3.7 Construction d’une ontologie................................................................... 38
2.7.1 Étapes de construction d’une ontologie ........................................... 38
2.7.2 Principes de construction d’ontologies............................................. 39
2.7.3 Environnements et outils de modélisation ....................................... 40
3.8 Conclusion ................................................................................................. 40
Partie II : Contribution
Chapitre 4 Spécification CTL basée Ontologie ................................................... 41
4.1 Introduction............................................................................................... 41
4.2 Proposition................................................................................................. 41
4.3 Méthode de construction de l’ontologie .................................................. 42
4.4 Etapes de développement ......................................................................... 44
4.4.1 Déterminer le domaine et la portée de l’ontologie .......................... 44
4.4.2 Envisager une éventuelle réutilisation des ontologies existantes... 45
4.4.3 Énumérer les termes importants dans l’ontologie .......................... 45
4.4.4 Définir les classes et la hiérarchie des classes.................................. 48
4.4.5 Définir les propriétés des classes (les attributs)............................... 49
4.4.6 Définir les facettes des attributs........................................................ 51
4.4.7 Réaliser les instances.......................................................................... 52
4.5 Discussion................................................................................................... 52
4.6 Conclusion ................................................................................................. 53
Chapitre 5 Analyse et Conception......................................................................... 54
5.1 Introduction............................................................................................... 54
5.2 Cahier de charges...................................................................................... 54
5.2.1 Introduction ........................................................................................ 54
5.2.2 Description générale........................................................................... 55
5.2.3 Spécification des besoins.................................................................... 55
5.3 Modélisation .............................................................................................. 56
5.3.1 Modélisation des fonctionnalités....................................................... 56
5.3.2 Modélisation de la dynamique .......................................................... 60
5.3.3 Modélisation de la structure.............................................................. 65
5.3.4 Modélisation des interactions............................................................ 66
5.4 Conclusion ................................................................................................. 71
Chapitre 6 Implémentation ................................................................................... 72
6.1 Introduction............................................................................................... 72
6.2 Langages et outils...................................................................................... 72
6.2.1 Java...................................................................................................... 72
6.2.2 SQWRL............................................................................................... 73
6.2.3 Jena...................................................................................................... 73
6.2.4 Eclipse.................................................................................................. 74
6.2.5 Protégé................................................................................................. 74
6.3 Implémentation de l’ontologie ................................................................. 75
6.3.1 Édition de l’ontologie ......................................................................... 75
6.3.2 Création des concepts ........................................................................ 75
6.3.3 Création des relations........................................................................ 76
6.3.4 Création d’attributs........................................................................... 77
6.3.5 Réalisation d’instances....................................................................... 77
6.3.6 Génération du graphe ........................................................................ 78
6.3.7 Génération du code OWL ................................................................. 79
6.4 Description de « Property-Specifier » ...................................................... 79
6.4.1 Vue principale..................................................................................... 80
6.4.2 Créer un nouveau projet ................................................................... 81
6.4.3 Ouvrir un projet existant................................................................... 82
6.4.4 Sauvegarder un projet....................................................................... 82
6.4.5 Gérer une propriété ........................................................................... 83
6.4.6 Ontology Based Assistant .................................................................. 83
6.4.7 Patterns Based Assistant.................................................................... 85
6.4.8 Help...................................................................................................... 88
6.5 Conclusion ................................................................................................. 88
Conclusion générale................................................................................................ 89Côte titre : MAI/0101 En ligne : https://drive.google.com/file/d/1QMDUS_FQ8jRmAjA-EmbQAA_4LzMnraum/view?usp=shari [...] Format de la ressource électronique : Assistant de spécification de propriétés a base d’ontologie [texte imprimé] / MEGUELATI ,Khadidja ; BOUAMARI,A, Directeur de thèse . - [S.l.] : Setif:UFA, 2016 . - 1 vol (91f.) ; 29 cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : Génie Logiciel
model-cheking
logique temporelle
patterns de spécification
ontologieIndex. décimale : 004 Informatique Résumé : Résumé
La spécification de propriétés à vérifier dans le cadre d’une vérification formelle par
model-checking est souvent difficile et nécessite des compétences spécialisées. Ce mémoire
présente une solution d'assistance basée sur les patterns de spécification et les ontologies et
propose une conception détaillée d’une solution logicielle de spécification assistée de
propriétés CTL. Le mémoire discute également les détails de réalisation de l’outil développé
Property-Specifier et les résultats obtenus.Note de contenu : Table des matières
Introduction générale ............................................................................................... 1
Partie I : Etat de l'art
Chapitre 1 Model-Checking
1.1 Introduction................................................................................................. 3
1.2 Vérification formelle................................................................................... 3
1.3 Model-Checking ........................................................................................... 4
1.3.1 Principes du Model-Checking.............................................................. 4
1.3.2 Outils du Model-Checking ................................................................... 5
1.3.3 Problèmes du Model-Checking............................................................ 5
1.4 Techniques de spécification........................................................................ 5
1.4.1 Logiques propositionnelles.................................................................. 6
1.4.2 Logiques temporelles ........................................................................... 6
1.4.3 Logiques temporelles temporisées...................................................... 6
1.5 Logique temporelle CTL............................................................................ 7
1.5.1 Le choix de CTL................................................................................... 7
1.5.2 Constituants de CTL............................................................................ 7
1.5.3 Classes de propriétés............................................................................ 9
1.5.4 Syntaxe de CTL.................................................................................... 9
1.5.5 Sémantique de CTL ............................................................................. 9
1.6 Conclusion ................................................................................................. 10
Chapitre 2 Spécification Assistée .................................Erreur ! Signet non défini.
2.1 Introduction............................................................................................... 11
2.2 Patterns de spécification........................................................................... 12
2.2.1 Classification des patterns................................................................. 13
2.2.2 Scopes (Portées des patterns)............................................................ 14
2.3 Travaux basés sur les patterns de spécification ..................................... 14
2.3.1 Support du choix des patterns .......................................................... 14
2.3.2 Nouvelles classifications des patterns............................................... 17
2.3.3 Autre assistants................................................................................... 19
2.3.4 Bilan sur l’utilisation des patterns.................................................... 21
2.4 Utilisations des ontologies dans la spécification des exigences ............. 22
2.4.1 Bilan sur l’utilisation des ontologies................................................. 26
2.5 Conclusion ................................................................................................. 27
Chapitre 3 Ontologies............................................................................................. 28
3.1 Introduction............................................................................................... 28
3.2 Apparition des ontologies......................................................................... 29
3.3 Définitions.................................................................................................. 29
3.4 Composants d’une ontologie .................................................................... 30
2.4.1 Concepts.............................................................................................. 30
2.4.2 Relations.............................................................................................. 31
2.4.3 Axiomes et instances .......................................................................... 32
3.5 Dimensions de classification des ontologies............................................ 33
2.5.1 Typologie selon l’objet de conceptualisation ................................... 33
2.5.2 Typologie selon le niveau de détails de l’ontologie.......................... 35
2.5.3 Typologie selon le niveau de complétude ......................................... 36
2.5.4 Typologie selon le niveau du formalisme ......................................... 36
3.6 OWL : le standard du Web sémantique ................................................. 37
3.7 Construction d’une ontologie................................................................... 38
2.7.1 Étapes de construction d’une ontologie ........................................... 38
2.7.2 Principes de construction d’ontologies............................................. 39
2.7.3 Environnements et outils de modélisation ....................................... 40
3.8 Conclusion ................................................................................................. 40
Partie II : Contribution
Chapitre 4 Spécification CTL basée Ontologie ................................................... 41
4.1 Introduction............................................................................................... 41
4.2 Proposition................................................................................................. 41
4.3 Méthode de construction de l’ontologie .................................................. 42
4.4 Etapes de développement ......................................................................... 44
4.4.1 Déterminer le domaine et la portée de l’ontologie .......................... 44
4.4.2 Envisager une éventuelle réutilisation des ontologies existantes... 45
4.4.3 Énumérer les termes importants dans l’ontologie .......................... 45
4.4.4 Définir les classes et la hiérarchie des classes.................................. 48
4.4.5 Définir les propriétés des classes (les attributs)............................... 49
4.4.6 Définir les facettes des attributs........................................................ 51
4.4.7 Réaliser les instances.......................................................................... 52
4.5 Discussion................................................................................................... 52
4.6 Conclusion ................................................................................................. 53
Chapitre 5 Analyse et Conception......................................................................... 54
5.1 Introduction............................................................................................... 54
5.2 Cahier de charges...................................................................................... 54
5.2.1 Introduction ........................................................................................ 54
5.2.2 Description générale........................................................................... 55
5.2.3 Spécification des besoins.................................................................... 55
5.3 Modélisation .............................................................................................. 56
5.3.1 Modélisation des fonctionnalités....................................................... 56
5.3.2 Modélisation de la dynamique .......................................................... 60
5.3.3 Modélisation de la structure.............................................................. 65
5.3.4 Modélisation des interactions............................................................ 66
5.4 Conclusion ................................................................................................. 71
Chapitre 6 Implémentation ................................................................................... 72
6.1 Introduction............................................................................................... 72
6.2 Langages et outils...................................................................................... 72
6.2.1 Java...................................................................................................... 72
6.2.2 SQWRL............................................................................................... 73
6.2.3 Jena...................................................................................................... 73
6.2.4 Eclipse.................................................................................................. 74
6.2.5 Protégé................................................................................................. 74
6.3 Implémentation de l’ontologie ................................................................. 75
6.3.1 Édition de l’ontologie ......................................................................... 75
6.3.2 Création des concepts ........................................................................ 75
6.3.3 Création des relations........................................................................ 76
6.3.4 Création d’attributs........................................................................... 77
6.3.5 Réalisation d’instances....................................................................... 77
6.3.6 Génération du graphe ........................................................................ 78
6.3.7 Génération du code OWL ................................................................. 79
6.4 Description de « Property-Specifier » ...................................................... 79
6.4.1 Vue principale..................................................................................... 80
6.4.2 Créer un nouveau projet ................................................................... 81
6.4.3 Ouvrir un projet existant................................................................... 82
6.4.4 Sauvegarder un projet....................................................................... 82
6.4.5 Gérer une propriété ........................................................................... 83
6.4.6 Ontology Based Assistant .................................................................. 83
6.4.7 Patterns Based Assistant.................................................................... 85
6.4.8 Help...................................................................................................... 88
6.5 Conclusion ................................................................................................. 88
Conclusion générale................................................................................................ 89Côte titre : MAI/0101 En ligne : https://drive.google.com/file/d/1QMDUS_FQ8jRmAjA-EmbQAA_4LzMnraum/view?usp=shari [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0101 MAI/0101 Mémoire Bibliothéque des sciences Français Disponible
Disponible
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
DisponibleModel-cheking mode des systèmes hiérarchiques / BOUGAHGOUH, Hamza
Titre : Model-cheking mode des systèmes hiérarchiques Type de document : texte imprimé Auteurs : BOUGAHGOUH, Hamza ; BOUAMARI,A, Directeur de thèse Editeur : Setif:UFA Année de publication : 2012 Importance : 1 vol (53f.) Format : 29 cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : Génie logiciel
méthode formelle
model-cheking
systhemes hiérarchique
MaudeIndex. décimale : 004 Informatique Côte titre : MAI/0035 Model-cheking mode des systèmes hiérarchiques [texte imprimé] / BOUGAHGOUH, Hamza ; BOUAMARI,A, Directeur de thèse . - [S.l.] : Setif:UFA, 2012 . - 1 vol (53f.) ; 29 cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : Génie logiciel
méthode formelle
model-cheking
systhemes hiérarchique
MaudeIndex. décimale : 004 Informatique Côte titre : MAI/0035 Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0035 MAI/0035 Mémoire Bibliothéque des sciences Français Disponible
Disponible
Titre : Spécification des propriétés temporelles à base d’ontologie Type de document : texte imprimé Auteurs : LAZIZI, Hana ; BOUAMARI,A, Directeur de thèse Editeur : Setif:UFA Année de publication : 2012 Importance : 1 vol (70f.) Format : 29 cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : Model-checking, Logique temporelle, Ontologie, Patterns de Spécification Index. décimale : 004 Informatique Résumé : Résumé
La spécification des propriétés à vérifier est une étape primordiale du processus de
vérification formelle par model-checking ou on utilise souvent les logiques temporelles
permettant d’affirmer l’évolution d’un système par rapport a un point de vue temporelle. Les
assistants à la spécification ont été mises en place afin de guider les utilisateurs des outils de
vérification dans l’objectif de mieux exprimer les exigences imposées sur le système dans une
logique temporelle donnée.
L’objectif de notre travail est l’utilisation des ontologies pour permettre une
génération automatique des formules de la logique temporelle LTL à partir d’une
spécification exprimée avec le langage naturel. Pour cela nous avons donné une proposition
de construction d’une ontologie du domaine de la sémantique LTL en basant sur les patterns
de spécification ce qui permet de développer un système d’aide pour générer les propriétés
LTL a partir d’une spécification en langage naturel.
Note de contenu : Sommaire
Introduction générale 1
Chapitre1 : La vérification formelle et le model-checking :
1.1. Introduction 4
1.2. Définitions et concepts de base 4
1.2.1. La vérification 4
1.2.2. Les méthodes semi-formelles 5
1.2.2.1. Le test 5
1.2.2.2. La simulation 6
1.2.3. Les méthodes formelles 6
1.2.3.1. La preuve formelle 7
1.2.3.2. Le model checking 7
1.3. Le model checking 8
1.3.1. Définition 8
1.3.2. Le processus du model checking 8
1.3.3. La spécification des propriétés 9
1.3.3.1. Les catégories des propriétés 9
1.3.3.2. Logique temporelle 10
1.3.3.2.1. Les logiques de temps linéaire (LTL, PLTL, ...) 11
1.3.3.2.2. La logique de temps arborescent 12
1.3.3.3. Les outils du model checking 13
1.4. Conclusion 14
Chapitre 2 : la logique de réécriture et le système Maude
2.1. Introduction 15
2.2. La logique de réécriture 15
2.2.1. La théorie de réécriture 16
2.2.2. Déduction dans la logique de réécriture 16
2.2.2.1. Principe de déduction 16
2.3. Le système Maude 16
2.3.1. Les niveaux de programmation en Maude 18
2 .3.2. Maude et le model checking 18
2.3.2.1. Une spécification système 18
2.3.2.2. Une spécification des propriétés 19
2.3.2.3. LTL et Maude 19
2.3.2.4. Structure de Kripke et Logique de Réécriture 19
2.3.2.5. L’application du Model Checking avec Maude 20
2.4. Conclusion 20
Chapitre3 : assistance a la spécification
3.1. Introduction 25
3.2. Les assistants à la spécification formelle 25
3.2.1. Les Patterns de Spécification 26
3.2.2. Extensions Temps-réel 28
3.2.3. Propel 29
3.3. Conclusion 29
Chapitre 4 : Les ontologies
4.1. Introduction 31
4.2. Notion d’ontologie 31
4.2.1. Définition 31
4.2.2. Constitution des ontologies 33
4.2.3. Les méthodologies de construction d’ontologies 37
4.2.3.1. La méthode SENSUS 37
4.2.3.2. La méthode KACTUS 37
4.2.3.3. La méthode METHONTOLOGY 38
4.2.3.4. La méthode "Ontology Development 101" 38
4.3. Conclusion 39
Chapitre 5 : construction d’une ontologie
5.1. Introduction 40
5.2. Travaux existants 40
5.3. La construction de l’ontologie 42
5.3.1. Méthodologie choisit 42
5.4. Conclusion 54
Chapitre 6 : conception UML
6.1. Introduction 55
6.2. Objectif du travail 55
6.3. L’architecture du système 56
6.4. La conception UML 57
6.4.2. Diagrammes de Séquences 57
6.5. Conclusion 58Côte titre : MAI/0028 En ligne : https://drive.google.com/file/d/1CWABUQDsyzf2dAGsg0OQU1FBp1V2YDEQ/view?usp=shari [...] Format de la ressource électronique : Spécification des propriétés temporelles à base d’ontologie [texte imprimé] / LAZIZI, Hana ; BOUAMARI,A, Directeur de thèse . - [S.l.] : Setif:UFA, 2012 . - 1 vol (70f.) ; 29 cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : Model-checking, Logique temporelle, Ontologie, Patterns de Spécification Index. décimale : 004 Informatique Résumé : Résumé
La spécification des propriétés à vérifier est une étape primordiale du processus de
vérification formelle par model-checking ou on utilise souvent les logiques temporelles
permettant d’affirmer l’évolution d’un système par rapport a un point de vue temporelle. Les
assistants à la spécification ont été mises en place afin de guider les utilisateurs des outils de
vérification dans l’objectif de mieux exprimer les exigences imposées sur le système dans une
logique temporelle donnée.
L’objectif de notre travail est l’utilisation des ontologies pour permettre une
génération automatique des formules de la logique temporelle LTL à partir d’une
spécification exprimée avec le langage naturel. Pour cela nous avons donné une proposition
de construction d’une ontologie du domaine de la sémantique LTL en basant sur les patterns
de spécification ce qui permet de développer un système d’aide pour générer les propriétés
LTL a partir d’une spécification en langage naturel.
Note de contenu : Sommaire
Introduction générale 1
Chapitre1 : La vérification formelle et le model-checking :
1.1. Introduction 4
1.2. Définitions et concepts de base 4
1.2.1. La vérification 4
1.2.2. Les méthodes semi-formelles 5
1.2.2.1. Le test 5
1.2.2.2. La simulation 6
1.2.3. Les méthodes formelles 6
1.2.3.1. La preuve formelle 7
1.2.3.2. Le model checking 7
1.3. Le model checking 8
1.3.1. Définition 8
1.3.2. Le processus du model checking 8
1.3.3. La spécification des propriétés 9
1.3.3.1. Les catégories des propriétés 9
1.3.3.2. Logique temporelle 10
1.3.3.2.1. Les logiques de temps linéaire (LTL, PLTL, ...) 11
1.3.3.2.2. La logique de temps arborescent 12
1.3.3.3. Les outils du model checking 13
1.4. Conclusion 14
Chapitre 2 : la logique de réécriture et le système Maude
2.1. Introduction 15
2.2. La logique de réécriture 15
2.2.1. La théorie de réécriture 16
2.2.2. Déduction dans la logique de réécriture 16
2.2.2.1. Principe de déduction 16
2.3. Le système Maude 16
2.3.1. Les niveaux de programmation en Maude 18
2 .3.2. Maude et le model checking 18
2.3.2.1. Une spécification système 18
2.3.2.2. Une spécification des propriétés 19
2.3.2.3. LTL et Maude 19
2.3.2.4. Structure de Kripke et Logique de Réécriture 19
2.3.2.5. L’application du Model Checking avec Maude 20
2.4. Conclusion 20
Chapitre3 : assistance a la spécification
3.1. Introduction 25
3.2. Les assistants à la spécification formelle 25
3.2.1. Les Patterns de Spécification 26
3.2.2. Extensions Temps-réel 28
3.2.3. Propel 29
3.3. Conclusion 29
Chapitre 4 : Les ontologies
4.1. Introduction 31
4.2. Notion d’ontologie 31
4.2.1. Définition 31
4.2.2. Constitution des ontologies 33
4.2.3. Les méthodologies de construction d’ontologies 37
4.2.3.1. La méthode SENSUS 37
4.2.3.2. La méthode KACTUS 37
4.2.3.3. La méthode METHONTOLOGY 38
4.2.3.4. La méthode "Ontology Development 101" 38
4.3. Conclusion 39
Chapitre 5 : construction d’une ontologie
5.1. Introduction 40
5.2. Travaux existants 40
5.3. La construction de l’ontologie 42
5.3.1. Méthodologie choisit 42
5.4. Conclusion 54
Chapitre 6 : conception UML
6.1. Introduction 55
6.2. Objectif du travail 55
6.3. L’architecture du système 56
6.4. La conception UML 57
6.4.2. Diagrammes de Séquences 57
6.5. Conclusion 58Côte titre : MAI/0028 En ligne : https://drive.google.com/file/d/1CWABUQDsyzf2dAGsg0OQU1FBp1V2YDEQ/view?usp=shari [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0028 MAI/0028 Mémoire Bibliothéque des sciences Français Disponible
DisponibleVérification formelle d'un protocole de l'accroissement de la longévité des réseaux de capteurs sons fil par des stations de base robustes / KHELLOUFI, ZAKARIA
Titre : Vérification formelle d'un protocole de l'accroissement de la longévité des réseaux de capteurs sons fil par des stations de base robustes Type de document : texte imprimé Auteurs : KHELLOUFI, ZAKARIA ; BOUAMARI,A, Directeur de thèse Editeur : Setif:UFA Année de publication : 2012 Importance : 1 vol (54f.) Format : 29 cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : réseaux de capteurs sans fils,tolérance aux fautes,station de base robustes,vérification formelle. Index. décimale : 004 Informatique Résumé : Résumé
Le domaine d’application des réseaux de capteurs sans fils ne cesse d’accroitre avec le besoin d’un mécanisme de tolérance aux fautes efficace. Le fait que les RCSF traitent des données très souvent sensibles, opérant dans des environnements hostiles et inattendus, la notion de la tolérance aux fautes est considérée comme indispensable.
Dans ce mémoire nous avons essayé de vérifier un protocole qui augment la durée de vie d’un réseaux de capteurs par des stations de base robustes.
Notre but, dans cette thèse est d’utiliser les techniques de la vérification formelle pour s’assurer que le protocole augmente la tolérance aux fautes de la station de primaire.Note de contenu : Table des matières
Chapitre 1 État de l’art ........................................
1. Introduction ......................................................
2. Qu’est-ce qu’un capteur sans fils ............................
2.1 Définition ............................................................
3. Architecture d'un RCSF .............................................
4. Station de base ..........................................................
4. Domaines d’applications des réseaux de capteurs ...........................
4.1 Applications militaires ................................................
4.2 Applications à la surveillance ........................................
4.3 Applications environnementales ..............................................
4.4 Applications médicales ................................................
5. Contraintes et caractéristiques liées aux réseaux de capteurs ........
6. Consommation d’énergie dans les RCSF .........................................
6.1 Energie de capture ...........................................................
6.2 Energie de traitement ............................................................
6.3 Energie de communication .....................................................
7. Catégories de communication .........................................................
8. Architectures adoptées pour les réseaux de capteurs ....................
9. Les défis des réseaux de capteurs ................................................
10. La tolérance aux fautes dans les réseaux de capteurs ...............
11. Les principaux protocoles de routage dans les RCSF ................
11.1 Les Protocoles hiérarchiques ...............................................
11.2 Les protocoles de routage basés sur la localisation ................
11.3 Les protocoles de routage ‘data-centric’ ..............................
12. Différentes problématiques dans les réseaux de capteurs ..........
13. Conclusion ....................................................................
Chapitre 2 vérification formelle et Maude .................................
1. vérification formelle ...................................................
1.1 Introduction.............................................................
1.3 Le mode-checking ...........................................
1.4 Les type de propriétés ............................................
1.4.1 Les propriétés de sûreté (safety) ou propriétés d’invariance
1.4.2 Les propriétés de vivacité (liveness) .................
1.4.3 Les propriétés d'équité (fairness).....................
Partie 2 Logique de Réécriture et Maude .................................
2 Logique de réécriture et Maude .............................................
2.1 introduction ...................................................................
2.2 Logique de Réécriture .......................................................
2.3 Langage Maude ...................................................................
2.3.1 Core Maude ....................................................
2.3.2 Full Maude .....................................................
2.4 Maude LTL Model-checker ..................................................
2.4.1 Niveau de spécification système ..................
2.4.2 Niveau de spécification des propriétés ...........
2.5 Model-checking avec Maude LTL model-checker .............
2.6 Real-Time Maude ...............................................................
2.10 Conclusion .....................................................................
Chapitre 3 Modélisation et spécifications ........................................
1. Introduction ..................................................................
2. Spécification du protocole .......................................................
3. Modélisation du protocole ........................................................
3.1 Modélisation de la station primaire .......................................
3.2 Modélisation de la station secondaire...................................
3.3 Modélisation du capteur ......................................................
4 Analyse du modèle ............................................................
4.1 Analyse du comportement de la station primaire ..................
4.2 Analyse du comportement de la Station secondaire ..............
4.3 analyse du comportement des Capteurs ..............................
5. Spécification des propriétés à vérifier .............................
5.1 Spécification informelle ...........................................
5.2 Spécification formelle des propriétés avec LTL.......................
6. CoChapitre 4 Réalisation ...................................................
1. Introduction ..........................................................
2. technologies et outils de développement ..................................
2.1 Eclipse.................................................................
2.1.1 avantages ..............................................................
2.2 Real-Time Maude .....................................................
2.2.1 Les étapes pour intégrer Real-Time-Maude dans Eclipse
3. Modélisation des stations de base ......................................
4. conclusions ............................................................
conclusion ............................................................
Côte titre : MAI/0007 En ligne : https://drive.google.com/file/d/15QBzc8xOjQA3pPfv6zDyYNa-0yyDIh2y/view?usp=shari [...] Format de la ressource électronique : Vérification formelle d'un protocole de l'accroissement de la longévité des réseaux de capteurs sons fil par des stations de base robustes [texte imprimé] / KHELLOUFI, ZAKARIA ; BOUAMARI,A, Directeur de thèse . - [S.l.] : Setif:UFA, 2012 . - 1 vol (54f.) ; 29 cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : réseaux de capteurs sans fils,tolérance aux fautes,station de base robustes,vérification formelle. Index. décimale : 004 Informatique Résumé : Résumé
Le domaine d’application des réseaux de capteurs sans fils ne cesse d’accroitre avec le besoin d’un mécanisme de tolérance aux fautes efficace. Le fait que les RCSF traitent des données très souvent sensibles, opérant dans des environnements hostiles et inattendus, la notion de la tolérance aux fautes est considérée comme indispensable.
Dans ce mémoire nous avons essayé de vérifier un protocole qui augment la durée de vie d’un réseaux de capteurs par des stations de base robustes.
Notre but, dans cette thèse est d’utiliser les techniques de la vérification formelle pour s’assurer que le protocole augmente la tolérance aux fautes de la station de primaire.Note de contenu : Table des matières
Chapitre 1 État de l’art ........................................
1. Introduction ......................................................
2. Qu’est-ce qu’un capteur sans fils ............................
2.1 Définition ............................................................
3. Architecture d'un RCSF .............................................
4. Station de base ..........................................................
4. Domaines d’applications des réseaux de capteurs ...........................
4.1 Applications militaires ................................................
4.2 Applications à la surveillance ........................................
4.3 Applications environnementales ..............................................
4.4 Applications médicales ................................................
5. Contraintes et caractéristiques liées aux réseaux de capteurs ........
6. Consommation d’énergie dans les RCSF .........................................
6.1 Energie de capture ...........................................................
6.2 Energie de traitement ............................................................
6.3 Energie de communication .....................................................
7. Catégories de communication .........................................................
8. Architectures adoptées pour les réseaux de capteurs ....................
9. Les défis des réseaux de capteurs ................................................
10. La tolérance aux fautes dans les réseaux de capteurs ...............
11. Les principaux protocoles de routage dans les RCSF ................
11.1 Les Protocoles hiérarchiques ...............................................
11.2 Les protocoles de routage basés sur la localisation ................
11.3 Les protocoles de routage ‘data-centric’ ..............................
12. Différentes problématiques dans les réseaux de capteurs ..........
13. Conclusion ....................................................................
Chapitre 2 vérification formelle et Maude .................................
1. vérification formelle ...................................................
1.1 Introduction.............................................................
1.3 Le mode-checking ...........................................
1.4 Les type de propriétés ............................................
1.4.1 Les propriétés de sûreté (safety) ou propriétés d’invariance
1.4.2 Les propriétés de vivacité (liveness) .................
1.4.3 Les propriétés d'équité (fairness).....................
Partie 2 Logique de Réécriture et Maude .................................
2 Logique de réécriture et Maude .............................................
2.1 introduction ...................................................................
2.2 Logique de Réécriture .......................................................
2.3 Langage Maude ...................................................................
2.3.1 Core Maude ....................................................
2.3.2 Full Maude .....................................................
2.4 Maude LTL Model-checker ..................................................
2.4.1 Niveau de spécification système ..................
2.4.2 Niveau de spécification des propriétés ...........
2.5 Model-checking avec Maude LTL model-checker .............
2.6 Real-Time Maude ...............................................................
2.10 Conclusion .....................................................................
Chapitre 3 Modélisation et spécifications ........................................
1. Introduction ..................................................................
2. Spécification du protocole .......................................................
3. Modélisation du protocole ........................................................
3.1 Modélisation de la station primaire .......................................
3.2 Modélisation de la station secondaire...................................
3.3 Modélisation du capteur ......................................................
4 Analyse du modèle ............................................................
4.1 Analyse du comportement de la station primaire ..................
4.2 Analyse du comportement de la Station secondaire ..............
4.3 analyse du comportement des Capteurs ..............................
5. Spécification des propriétés à vérifier .............................
5.1 Spécification informelle ...........................................
5.2 Spécification formelle des propriétés avec LTL.......................
6. CoChapitre 4 Réalisation ...................................................
1. Introduction ..........................................................
2. technologies et outils de développement ..................................
2.1 Eclipse.................................................................
2.1.1 avantages ..............................................................
2.2 Real-Time Maude .....................................................
2.2.1 Les étapes pour intégrer Real-Time-Maude dans Eclipse
3. Modélisation des stations de base ......................................
4. conclusions ............................................................
conclusion ............................................................
Côte titre : MAI/0007 En ligne : https://drive.google.com/file/d/15QBzc8xOjQA3pPfv6zDyYNa-0yyDIh2y/view?usp=shari [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0007 MAI/0007 Mémoire Bibliothéque des sciences Français Disponible
Disponible