University Sétif 1 FERHAT ABBAS Faculty of Sciences
Résultat de la recherche
1 résultat(s) recherche sur le mot-clé '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 étendue'
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 : 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