University Sétif 1 FERHAT ABBAS Faculty of Sciences
Détail de l'auteur
Auteur KhelaLfa,Farah |
Documents disponibles écrits par cet auteur
Ajouter le résultat dans votre panier Affiner la recherche
Titre : Inter-procedural analysis by model checking Type de document : texte imprimé Auteurs : KhelaLfa,Farah, Auteur ; Bouamari,Abdelkader, Directeur de thèse Editeur : Setif:UFA Année de publication : 2019 Importance : 1 vol (46 f .) Format : 29 cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : Vérification formelle
Model-Checking CTL
Modélisation du système
Structure de Kripke
Appels récursifs
Programme procéduraux
Machine d’états récursive étendueIndex. décimale : 004 - Informatique Résumé : L'analyse statique de modèle-checking de programmes avec des appels procéduraux et récursifs est souvent peu pratique en raison du problème de l'explosion de l'espace d'état. Notre projet vise à développer un outil de modèle-checking qui adapte l'algorithme de vérification de modèle CTL aux programmes permettant des appels procéduraux et récursifs. Cette vérification des procédures par CTL modèle-checking est souvent difficile et nécessite des structures ou des algorithmes adaptés. Note de contenu : Sommaire
General Introduction ................................................................................................... 1
Chapter â… : System verification
I.1 Introduction ............................................................................................................ 3
I.2 Formal verification ................................................................................................. 3
I.3 Principles of Model Checking ............................................................................... 3
3.1. System modeling ............................................................................................. 4
3.1.1. Transition system ..................................................................................... 4
3.1.2. Kripke structure ........................................................................................ 6
3.2. Specification of properties ............................................................................... 7
3.2.1. Linear temporal logic ................................................................................... 7
3.2.2. Computational tree logic .............................................................................. 8
I.4 Verification .............................................................................................................. 9
4.1. Model checking LTL ....................................................................................... 9
4.2. Model checking LTL ....................................................................................... 9
I.5 Symbolic model checking ..................................................................................... 10
I.6 Conclusion ............................................................................................................. 10
Chapter â…¡: Procedural analysis of programs
II.1 Introduction ......................................................................................................... 11
II.2 Analysis of reactive systems ............................................................................... 11
II.3 Structured program ............................................................................................ 12
3.1. Structure ............................................................................................................ 12
3.1.1. Program schemata .................................................................................. 12
3.2. Analysis by model checking .......................................................................... 15
II.4 Procedural program ........................................................................................... 15
4.1. Structure ............................................................................................................ 15
4.2. Models of Procedural Programs .................................................................... 16
4.3. State of the art of model-checking analysis of procedural programs ............ 17
4.3.1. Search for publications ........................................................................... 17
4.3.2. Results analysis ...................................................................................... 17
4.3.3. Keywording and Mapping ...................................................................... 24
II.4 Conclusion ........................................................................................................... 25
Chapter â…¢: Contribution
III.1 Introduction ....................................................................................................... 26
III.2 Formal description ............................................................................................ 26
2.1. Formal description general structure of a program ....................................... 26
2.2. Formal exit description .................................................................................. 28
III.3 Algorithm transforming programs into ERSM .............................................. 29
III.4 Hierarchical Kripke Structure ......................................................................... 31
III.4 Verification by CTL model checking algorithm ............................................. 31
III.6 Conclusion .......................................................................................................... 32
Chapter â…£: Analysis and design
IV.1 Introduction ....................................................................................................... 33
IV.2 Specification ....................................................................................................... 33
2.1. Objectives ....................................................................................................... 33
2.2. Requirement specification .............................................................................. 33
2.3 General description ......................................................................................... 34
IV.3 Analysis and design ........................................................................................... 35
3.1. Use case diagram ............................................................................................. 35
3.2. Class diagram .................................................................................................. 37
3.3. Sequence diagrams .......................................................................................... 37
IV.4 Conclusion .......................................................................................................... 40
Chapter â…¤: Implementation
V.1 Introduction ......................................................................................................... 41
V.2 Environment ........................................................................................................ 41
2.1. Choice of java ................................................................................................ 41
2.2. Choice of NetBeans ....................................................................................... 41
2.3. Steps .............................................................................................................. 42
V.3 Implementation of the proposed solution ......................................................... 42
V.4 Implementation of the proposed solution ......................................................... 42
V.5 Conclusion ............................................................................................................ 45
General conclusion ..................................................................................................... 44
Bibliography ...............................................................................................................Côte titre : MAI/0302 En ligne : https://drive.google.com/file/d/1m3VulTOIWWKXd2r4CVF7tXQvYuP4kij0/view?usp=shari [...] Format de la ressource électronique : Inter-procedural analysis by model checking [texte imprimé] / KhelaLfa,Farah, Auteur ; Bouamari,Abdelkader, Directeur de thèse . - [S.l.] : Setif:UFA, 2019 . - 1 vol (46 f .) ; 29 cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : Vérification formelle
Model-Checking CTL
Modélisation du système
Structure de Kripke
Appels récursifs
Programme procéduraux
Machine d’états récursive étendueIndex. décimale : 004 - Informatique Résumé : L'analyse statique de modèle-checking de programmes avec des appels procéduraux et récursifs est souvent peu pratique en raison du problème de l'explosion de l'espace d'état. Notre projet vise à développer un outil de modèle-checking qui adapte l'algorithme de vérification de modèle CTL aux programmes permettant des appels procéduraux et récursifs. Cette vérification des procédures par CTL modèle-checking est souvent difficile et nécessite des structures ou des algorithmes adaptés. Note de contenu : Sommaire
General Introduction ................................................................................................... 1
Chapter â… : System verification
I.1 Introduction ............................................................................................................ 3
I.2 Formal verification ................................................................................................. 3
I.3 Principles of Model Checking ............................................................................... 3
3.1. System modeling ............................................................................................. 4
3.1.1. Transition system ..................................................................................... 4
3.1.2. Kripke structure ........................................................................................ 6
3.2. Specification of properties ............................................................................... 7
3.2.1. Linear temporal logic ................................................................................... 7
3.2.2. Computational tree logic .............................................................................. 8
I.4 Verification .............................................................................................................. 9
4.1. Model checking LTL ....................................................................................... 9
4.2. Model checking LTL ....................................................................................... 9
I.5 Symbolic model checking ..................................................................................... 10
I.6 Conclusion ............................................................................................................. 10
Chapter â…¡: Procedural analysis of programs
II.1 Introduction ......................................................................................................... 11
II.2 Analysis of reactive systems ............................................................................... 11
II.3 Structured program ............................................................................................ 12
3.1. Structure ............................................................................................................ 12
3.1.1. Program schemata .................................................................................. 12
3.2. Analysis by model checking .......................................................................... 15
II.4 Procedural program ........................................................................................... 15
4.1. Structure ............................................................................................................ 15
4.2. Models of Procedural Programs .................................................................... 16
4.3. State of the art of model-checking analysis of procedural programs ............ 17
4.3.1. Search for publications ........................................................................... 17
4.3.2. Results analysis ...................................................................................... 17
4.3.3. Keywording and Mapping ...................................................................... 24
II.4 Conclusion ........................................................................................................... 25
Chapter â…¢: Contribution
III.1 Introduction ....................................................................................................... 26
III.2 Formal description ............................................................................................ 26
2.1. Formal description general structure of a program ....................................... 26
2.2. Formal exit description .................................................................................. 28
III.3 Algorithm transforming programs into ERSM .............................................. 29
III.4 Hierarchical Kripke Structure ......................................................................... 31
III.4 Verification by CTL model checking algorithm ............................................. 31
III.6 Conclusion .......................................................................................................... 32
Chapter â…£: Analysis and design
IV.1 Introduction ....................................................................................................... 33
IV.2 Specification ....................................................................................................... 33
2.1. Objectives ....................................................................................................... 33
2.2. Requirement specification .............................................................................. 33
2.3 General description ......................................................................................... 34
IV.3 Analysis and design ........................................................................................... 35
3.1. Use case diagram ............................................................................................. 35
3.2. Class diagram .................................................................................................. 37
3.3. Sequence diagrams .......................................................................................... 37
IV.4 Conclusion .......................................................................................................... 40
Chapter â…¤: Implementation
V.1 Introduction ......................................................................................................... 41
V.2 Environment ........................................................................................................ 41
2.1. Choice of java ................................................................................................ 41
2.2. Choice of NetBeans ....................................................................................... 41
2.3. Steps .............................................................................................................. 42
V.3 Implementation of the proposed solution ......................................................... 42
V.4 Implementation of the proposed solution ......................................................... 42
V.5 Conclusion ............................................................................................................ 45
General conclusion ..................................................................................................... 44
Bibliography ...............................................................................................................Côte titre : MAI/0302 En ligne : https://drive.google.com/file/d/1m3VulTOIWWKXd2r4CVF7tXQvYuP4kij0/view?usp=shari [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0302 MAI/0302 Mémoire Bibliothéque des sciences Français Disponible
Disponible