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 étendue
Index. 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 :	pdf

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 étendue
Index. 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 :	pdf