University Sétif 1 FERHAT ABBAS Faculty of Sciences
Détail de l'auteur
Auteur Messous ,Randa |
Documents disponibles écrits par cet auteur
Ajouter le résultat dans votre panier Affiner la rechercheUn outil de transformation automatique d’un réseau de Petri vers la logique de réécriture / Messous ,Randa
Titre : Un outil de transformation automatique d’un réseau de Petri vers la logique de réécriture Type de document : texte imprimé Auteurs : Messous ,Randa, Auteur ; Khabbaba ,Abdellah, Directeur de thèse Editeur : Setif:UFA Année de publication : 2019 Importance : 1 vol (48 f .) Format : 29 cm Catégories : Thèses & Mémoires:Informatique Mots-clés : Réseaux de Pétri
Maude
Logique de réécriture
LTL model-checkerIndex. décimale : 004 - Informatique Résumé :
Les réseaux de Petri représentent un outil extrêmement utile dans le domaine de la modélisation et de vérification des systèmes. En dépit de leur pouvoir d'analyse, il offre une représentation graphique simple qui facilite parfaitement la manipulation et l’analyse des systèmes dynamiques.
Ce mémoire présente une méthodologie de spécification et de vérification des réseaux de Petri en utilisant le système Maude. L’objectif de notre projet est présenter l’apport du formalisme de la logique de réécriture dans la vérification d’un certain nombre de propriétés des modèles basés sur les réseaux de Petri. Ceci a été accompli pratiquement via son outil d’analyse LTL model-checker.Note de contenu :
Sommaire
ntroduction général……………………………………………………………………………1
Chapitre 1
1. Introduction ............................................................................................................ 3
2. Principe du model-checking ................................................................................... 3
2.2. Classification des propriétés à vérifier ............................................................ 5
3. Model-checking LTL .............................................................................................. 6
4. Outils de model-Checking ...................................................................................... 8
4.1. SMV ................................................................................................................ 8
4.2. SPIN ................................................................................................................ 8
4.3. Model-checker LTL de Maude ....................................................................... 9
5. Limitations et solutions ........................................................................................ 10
5.1. Explosion de l’espace d’état .......................................................................... 10
5.2. Solution Symbolique ..................................................................................... 10
6. Conclusion ............................................................................................................ 11
Chapitre 2
1. Introduction .......................................................................................................... 13
2. Logique de réécriture ............................................................................................
2.1. Introduction ................................................................................................... 1
2.2. Théorie de réécriture ..................................................................................... 14
2.3. Règles de déduction ...................................................................................... 15
1. La réflexivité ................................................................................................. 16
3. Le remplacement .............................................................................................. 16
4. La transitivité ............................................................................................... 16
2.4. Réécriture Concurrente ................................................................................. 18
3. Le système Maude ................................................................................................ 19
3.1. Syntaxe de Maude ......................................................................................... 20
3.1.1. La déclaration des sortes et sous-sortes ................................................. 20
3.1.2. Les variables .......................................................................................... 21
3.1.3. Déclaration des opérations ..................................................................... 21
3.1.4. Déclaration des équations ...................................................................... 21
3.1.5. Déclaration des règles de réécriture ....................................................... 22
3.2. Modules Maude ............................................................................................. 22
3.2.1. Module fonctionnel ................................................................................ 22
3.2.2. Module système ..................................................................................... 23
3.2.3. Module orienté-objet .............................................................................. 25
3.2.4. Modules prédéfinis................................................................................. 25
3.3. module model-cheking Maude ...................................................................... 26
4. Conclusion ............................................................................................................ 27
Chapitre 3
1. Introduction .......................................................................................................... 29
2. Réseaux de Petri ...................................................................................................
2.1. Définition ......................................................................................................
2.2. Sémantique .................................................................................................... 30
3. Réseaux de Petri sur Maude ................................................................................. 32
3.1. Réseaux de Petri dans la logique de réécriture .............................................. 32
4. Model-checking et RDPs : état de l’art ................................................................ 33
4.1. Travaux voisins ............................................................................................. 34
4.2. Propriétés à vérifier ....................................................................................... 35
5. Conclusion ............................................................................................................ 36
Chapitre 4
1. Introduction .......................................................................................................... 38
2. Système de contrôle d’accès ................................................................................. 38
2.1 Contrôle d’accès ............................................................................................ 38
2.2 Architecture du système ................................................................................ 39
2.3 Principe..........................................................................................................
2.4 Propriétés du système .................................................................................... 41
3. ÉTUDE DE CAS .................................................................................................. 41
3.1 Description générale du système ................................................................... 41
3.2. Spécifications Maude .................................................................................... 42
3.2.1. Spécification du système........................................................................ 42
3.2.2. Spécification des propriétés ................................................................... 43
3.2.3. Verification ............................................................................................ 44
3.3. Conclusion ..................................................................................................... 4
Conclusion général…………………………………………………………………...47
Bibliographie…………………………………………………………………………48Côte titre : MAI/0339 En ligne : https://drive.google.com/file/d/1KW6KzGhb2AgfScujU51y39KOlcha7zL6/view?usp=shari [...] Format de la ressource électronique : Un outil de transformation automatique d’un réseau de Petri vers la logique de réécriture [texte imprimé] / Messous ,Randa, Auteur ; Khabbaba ,Abdellah, Directeur de thèse . - [S.l.] : Setif:UFA, 2019 . - 1 vol (48 f .) ; 29 cm.
Catégories : Thèses & Mémoires:Informatique Mots-clés : Réseaux de Pétri
Maude
Logique de réécriture
LTL model-checkerIndex. décimale : 004 - Informatique Résumé :
Les réseaux de Petri représentent un outil extrêmement utile dans le domaine de la modélisation et de vérification des systèmes. En dépit de leur pouvoir d'analyse, il offre une représentation graphique simple qui facilite parfaitement la manipulation et l’analyse des systèmes dynamiques.
Ce mémoire présente une méthodologie de spécification et de vérification des réseaux de Petri en utilisant le système Maude. L’objectif de notre projet est présenter l’apport du formalisme de la logique de réécriture dans la vérification d’un certain nombre de propriétés des modèles basés sur les réseaux de Petri. Ceci a été accompli pratiquement via son outil d’analyse LTL model-checker.Note de contenu :
Sommaire
ntroduction général……………………………………………………………………………1
Chapitre 1
1. Introduction ............................................................................................................ 3
2. Principe du model-checking ................................................................................... 3
2.2. Classification des propriétés à vérifier ............................................................ 5
3. Model-checking LTL .............................................................................................. 6
4. Outils de model-Checking ...................................................................................... 8
4.1. SMV ................................................................................................................ 8
4.2. SPIN ................................................................................................................ 8
4.3. Model-checker LTL de Maude ....................................................................... 9
5. Limitations et solutions ........................................................................................ 10
5.1. Explosion de l’espace d’état .......................................................................... 10
5.2. Solution Symbolique ..................................................................................... 10
6. Conclusion ............................................................................................................ 11
Chapitre 2
1. Introduction .......................................................................................................... 13
2. Logique de réécriture ............................................................................................
2.1. Introduction ................................................................................................... 1
2.2. Théorie de réécriture ..................................................................................... 14
2.3. Règles de déduction ...................................................................................... 15
1. La réflexivité ................................................................................................. 16
3. Le remplacement .............................................................................................. 16
4. La transitivité ............................................................................................... 16
2.4. Réécriture Concurrente ................................................................................. 18
3. Le système Maude ................................................................................................ 19
3.1. Syntaxe de Maude ......................................................................................... 20
3.1.1. La déclaration des sortes et sous-sortes ................................................. 20
3.1.2. Les variables .......................................................................................... 21
3.1.3. Déclaration des opérations ..................................................................... 21
3.1.4. Déclaration des équations ...................................................................... 21
3.1.5. Déclaration des règles de réécriture ....................................................... 22
3.2. Modules Maude ............................................................................................. 22
3.2.1. Module fonctionnel ................................................................................ 22
3.2.2. Module système ..................................................................................... 23
3.2.3. Module orienté-objet .............................................................................. 25
3.2.4. Modules prédéfinis................................................................................. 25
3.3. module model-cheking Maude ...................................................................... 26
4. Conclusion ............................................................................................................ 27
Chapitre 3
1. Introduction .......................................................................................................... 29
2. Réseaux de Petri ...................................................................................................
2.1. Définition ......................................................................................................
2.2. Sémantique .................................................................................................... 30
3. Réseaux de Petri sur Maude ................................................................................. 32
3.1. Réseaux de Petri dans la logique de réécriture .............................................. 32
4. Model-checking et RDPs : état de l’art ................................................................ 33
4.1. Travaux voisins ............................................................................................. 34
4.2. Propriétés à vérifier ....................................................................................... 35
5. Conclusion ............................................................................................................ 36
Chapitre 4
1. Introduction .......................................................................................................... 38
2. Système de contrôle d’accès ................................................................................. 38
2.1 Contrôle d’accès ............................................................................................ 38
2.2 Architecture du système ................................................................................ 39
2.3 Principe..........................................................................................................
2.4 Propriétés du système .................................................................................... 41
3. ÉTUDE DE CAS .................................................................................................. 41
3.1 Description générale du système ................................................................... 41
3.2. Spécifications Maude .................................................................................... 42
3.2.1. Spécification du système........................................................................ 42
3.2.2. Spécification des propriétés ................................................................... 43
3.2.3. Verification ............................................................................................ 44
3.3. Conclusion ..................................................................................................... 4
Conclusion général…………………………………………………………………...47
Bibliographie…………………………………………………………………………48Côte titre : MAI/0339 En ligne : https://drive.google.com/file/d/1KW6KzGhb2AgfScujU51y39KOlcha7zL6/view?usp=shari [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0339 MAI/0339 Mémoire Bibliothéque des sciences Français Disponible
Disponible
