University Sétif 1 FERHAT ABBAS Faculty of Sciences
Résultat de la recherche
1 résultat(s) recherche sur le mot-clé 'Model-checking, Logique temporelle, Ontologie, Patterns de Spécification'
Ajouter le résultat dans votre panier Affiner la recherche Générer le flux rss de la recherche
Partager le résultat de cette recherche
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
Disponible