University Sétif 1 FERHAT ABBAS Faculty of Sciences
Détail de l'auteur
Auteur Bouamari,Abdelkader |
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
Titre : Model-checking de modèles hiérarchiques Type de document : texte imprimé Auteurs : Boukhers, Ibtissem, Auteur ; Bouamari,Abdelkader, Directeur de thèse Editeur : Setif:UFA Année de publication : 2019 Importance : 1 vol (61 f .) Format : 29 cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : Vérification formelle
Model-Checking hiérarchiqueIndex. décimale : 004 - Informatique Résumé : La technique d’analyse de modèles par Model-Checking s'applique souvent sur des modèles de machines d'états aplatis (non-hiérarchiques), et ne propose aucun support pour des modèles hiérarchiques tels que les statecharts et les machines d'états UML. Ce mémoire propose une solution basée sur l'aplatissement pour analyser formellement des modèles hiérarchiques formalisés avec des structures de Kripke. Il décrit dans ce contexte la conception détaillée et l'implémentation de la solution logicielle ‘’Flattening Hierarchical Model-Checker’’ développée. Note de contenu :
Sommaire
Keywords .................................................................................................................. i
Résumé ........................................................................................................................... i
Introduction générale .................................................................................................. 1
I.1 Introduction ............................................................................................................ 3
I.2 Model-Checking ...................................................................................................... 3
I.3 Principes du Model-Checking ............................................................................... 3
I.4 Modélisation du comportement ............................................................................ 4
4.1. Système d’automate ....................................................................................... 4
4.2. Structure de Kripke ...................................................................................... 5
I.5 Spécification des propriétés .......................................................................6
5.1. Logique temporelle linéaire .............................................................................. 6
5.2. Logique temporelle arborescente ..................................................................... 7
I.6 Vérification .............................................................................................................. 9
6.1. Model-Checking de LTL .................................................................................. 9
6.2. Model-Checking de CTL ................................................................................. 9
I.7 Model-Cheking symbolique ................................................................................. 11
I.8 Conclusion ............................................................................................................. 12
II.1 Introduction ......................................................................................................... 13
II.2 Motivation ............................................................................................................ 13
II.3 Modèle Statecharts ........................................................................... 1
3.1. Sémantique des Statecharts ............................................................................ 15
II.4 Défis du Model-checking en présence de la hiérarchie ................................... 16
II.5 Travaux connexes ....................................................................... 1
5.1. Technique sans aplatissement ........................................................................ 18
5.2. Techniques avec aplatissement ...................................................................... 23
5.2.1 Model-Checking de Statechart transformé en SMV : ............................... 24
5.2.2 Model-Checking des Statecharts traduit en SPIN: .................................... 31
5.2.3 Environnement de verification des STATEMENT .................................... 35
5.2.4 Vérification des Statecharts avec ESTEREL .............................................. 36
5.2.5 Vérification des State machines réactifs et communicants ........................ 36
5.2.6 Exploitation de la hiérarchie comportementale pour une vérification efficace par Model........................................................................................ 37
II.6 Comparaison des techniques .............................................................................. 38
II.7 Conclusion ........................................................................................................... 39
III.1 Introduction ....................................................................................................... 40
III.2 Déscription formelle ......................................................................... 4
2.1. Déscription générale du système ................................................................ 40
2.2. Structure de kripke hiérarchique .............................................................. 42
III.3 Algorithme d’aplatissement ............................................................................. 43
III.4 Struture de Kripke aplatie ............................................................................... 45
III.5 Conclusion .......................................................................................................... 46
IV.1 Introduction ....................................................................................................... 47
IV.2 Cahier de charges .................................................................................... 4
2.1. Objectifs .......................................................................................................... 47
2.2. Spécification des besoins ................................................................................. 47
2.3. Déscription générale ........................................................................................ 49
IV.3 Analyse et conception ........................................................................................ 49
3.1. Diagramme de cas d’utilisation ...................................................................... 49
3.2. Diagramme de classe ....................................................................................... 50
3.3. Diagramme de séquence ................................................................................. 51
3.4. Diagramme d’activité ...................................................................................... 53
IV.4 Conclusion .......................................................................................................... 54
V.1 Introduction ......................................................................................................... 55
V.2 Environnement ....................................................................................................
2.1. Choix de java................................................................................................ 55
Choix de Eclipse......................................................................
55 2.4.
Démarche......................................................................................................
56 V.3 Implementation de la solution proposée
56 V.4 Évaluation des résultats
......................................................................................
Conclusion............................................................................................
61 Conclusion générale
...................................................................................................
62 Références Bibliographiques.....................................................................................
64 2.3 Choix du XML....................................................................................Côte titre : MAI/0338 En ligne : https://drive.google.com/file/d/1qw6I7KClZ73S94mEwXwolSP44nuGQpyE/view?usp=shari [...] Format de la ressource électronique : Model-checking de modèles hiérarchiques [texte imprimé] / Boukhers, Ibtissem, Auteur ; Bouamari,Abdelkader, Directeur de thèse . - [S.l.] : Setif:UFA, 2019 . - 1 vol (61 f .) ; 29 cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : Vérification formelle
Model-Checking hiérarchiqueIndex. décimale : 004 - Informatique Résumé : La technique d’analyse de modèles par Model-Checking s'applique souvent sur des modèles de machines d'états aplatis (non-hiérarchiques), et ne propose aucun support pour des modèles hiérarchiques tels que les statecharts et les machines d'états UML. Ce mémoire propose une solution basée sur l'aplatissement pour analyser formellement des modèles hiérarchiques formalisés avec des structures de Kripke. Il décrit dans ce contexte la conception détaillée et l'implémentation de la solution logicielle ‘’Flattening Hierarchical Model-Checker’’ développée. Note de contenu :
Sommaire
Keywords .................................................................................................................. i
Résumé ........................................................................................................................... i
Introduction générale .................................................................................................. 1
I.1 Introduction ............................................................................................................ 3
I.2 Model-Checking ...................................................................................................... 3
I.3 Principes du Model-Checking ............................................................................... 3
I.4 Modélisation du comportement ............................................................................ 4
4.1. Système d’automate ....................................................................................... 4
4.2. Structure de Kripke ...................................................................................... 5
I.5 Spécification des propriétés .......................................................................6
5.1. Logique temporelle linéaire .............................................................................. 6
5.2. Logique temporelle arborescente ..................................................................... 7
I.6 Vérification .............................................................................................................. 9
6.1. Model-Checking de LTL .................................................................................. 9
6.2. Model-Checking de CTL ................................................................................. 9
I.7 Model-Cheking symbolique ................................................................................. 11
I.8 Conclusion ............................................................................................................. 12
II.1 Introduction ......................................................................................................... 13
II.2 Motivation ............................................................................................................ 13
II.3 Modèle Statecharts ........................................................................... 1
3.1. Sémantique des Statecharts ............................................................................ 15
II.4 Défis du Model-checking en présence de la hiérarchie ................................... 16
II.5 Travaux connexes ....................................................................... 1
5.1. Technique sans aplatissement ........................................................................ 18
5.2. Techniques avec aplatissement ...................................................................... 23
5.2.1 Model-Checking de Statechart transformé en SMV : ............................... 24
5.2.2 Model-Checking des Statecharts traduit en SPIN: .................................... 31
5.2.3 Environnement de verification des STATEMENT .................................... 35
5.2.4 Vérification des Statecharts avec ESTEREL .............................................. 36
5.2.5 Vérification des State machines réactifs et communicants ........................ 36
5.2.6 Exploitation de la hiérarchie comportementale pour une vérification efficace par Model........................................................................................ 37
II.6 Comparaison des techniques .............................................................................. 38
II.7 Conclusion ........................................................................................................... 39
III.1 Introduction ....................................................................................................... 40
III.2 Déscription formelle ......................................................................... 4
2.1. Déscription générale du système ................................................................ 40
2.2. Structure de kripke hiérarchique .............................................................. 42
III.3 Algorithme d’aplatissement ............................................................................. 43
III.4 Struture de Kripke aplatie ............................................................................... 45
III.5 Conclusion .......................................................................................................... 46
IV.1 Introduction ....................................................................................................... 47
IV.2 Cahier de charges .................................................................................... 4
2.1. Objectifs .......................................................................................................... 47
2.2. Spécification des besoins ................................................................................. 47
2.3. Déscription générale ........................................................................................ 49
IV.3 Analyse et conception ........................................................................................ 49
3.1. Diagramme de cas d’utilisation ...................................................................... 49
3.2. Diagramme de classe ....................................................................................... 50
3.3. Diagramme de séquence ................................................................................. 51
3.4. Diagramme d’activité ...................................................................................... 53
IV.4 Conclusion .......................................................................................................... 54
V.1 Introduction ......................................................................................................... 55
V.2 Environnement ....................................................................................................
2.1. Choix de java................................................................................................ 55
Choix de Eclipse......................................................................
55 2.4.
Démarche......................................................................................................
56 V.3 Implementation de la solution proposée
56 V.4 Évaluation des résultats
......................................................................................
Conclusion............................................................................................
61 Conclusion générale
...................................................................................................
62 Références Bibliographiques.....................................................................................
64 2.3 Choix du XML....................................................................................Côte titre : MAI/0338 En ligne : https://drive.google.com/file/d/1qw6I7KClZ73S94mEwXwolSP44nuGQpyE/view?usp=shari [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0338 MAI/0338 Mémoire Bibliothéque des sciences Français Disponible
Disponible
Titre : Model-cheeking de formules ltl à base d'automates Type de document : texte imprimé Auteurs : Merir,Hdjer, Auteur ; Bouamari,Abdelkader, Directeur de thèse Editeur : Setif:UFA Année de publication : 2018 Importance : 1 vol (44 f .) Format : 29 cm Langues : Français (fre) Langues originales : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : Model-checking
Structures de kripke
Logique temorelle ltl
Automate de buchiIndex. décimale : 004 Informatique Note de contenu :
Sommaire
Table des figures
Introduction générale
Versification des logiciels
Model-checking
Model- checking ltl
Implémentation d'un model checking ltl
Conclusion générale
Côte titre : MAI/0252 Model-cheeking de formules ltl à base d'automates [texte imprimé] / Merir,Hdjer, Auteur ; Bouamari,Abdelkader, Directeur de thèse . - [S.l.] : Setif:UFA, 2018 . - 1 vol (44 f .) ; 29 cm.
Langues : Français (fre) Langues originales : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : Model-checking
Structures de kripke
Logique temorelle ltl
Automate de buchiIndex. décimale : 004 Informatique Note de contenu :
Sommaire
Table des figures
Introduction générale
Versification des logiciels
Model-checking
Model- checking ltl
Implémentation d'un model checking ltl
Conclusion générale
Côte titre : MAI/0252 Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0252 MAI/0252 Mémoire Bibliothéque des sciences Français Disponible
Disponible
Titre : UFAS - Academy Portal Type de document : texte imprimé Auteurs : Ahmed saad eddine Fellahi, Auteur ; mohamed lamine Chiheb, Auteur ; Bouamari,Abdelkader, Directeur de thèse Editeur : Sétif:UFA1 Année de publication : 2023 Importance : 1 vol (52 f .) Format : 29cm Langues : Français (fre) Catégories : Thèses & Mémoires:Informatique Mots-clés : E-learning
Plateforme d’apprentissageIndex. décimale : 004 Informatique Résumé : Les progrès des Technologies de l'Information et de la Communication (TIC) ont conduit à de nouveaux modes d’apprentissage, en particulier dans le domaine de l’éducation, tels que l’apprentissage à distance, également connu sous le nom d’apprentissage électronique. Cette approche implique l’utilisation de moyens de communication et de multimédia dans le processus éducatif. L’éducation à distance est devenue une solution fondamentale dans les cas où les restrictions de temps et d’espace sont problématiques ou impossibles, comme ce fut le cas avec la propagation de la pandémie de COVID-19.
Dans le cadre de ce projet, une plateforme d’apprentissage en ligne pour l’université de SETIF est développée sur la base du framework Laravel. Les étudiants et les enseignants peuvent s’inscrire à cette plateforme, où les enseignants peuvent afficher des cours et les étudiants peuvent les suivre. Les étudiants peuvent également évaluer leurs connaissances en posant des questions sur des informations incompréhensibles L’administrateur gère les différentes ressources de la plateforme ainsi que les et les droits d’accès des différents utilisateursCôte titre : MAI/0725 En ligne : https://drive.google.com/file/d/1bWs3pyQclSSUajYLkSmO-98tqhNza-sa/view?usp=drive [...] Format de la ressource électronique : UFAS - Academy Portal [texte imprimé] / Ahmed saad eddine Fellahi, Auteur ; mohamed lamine Chiheb, Auteur ; Bouamari,Abdelkader, Directeur de thèse . - [S.l.] : Sétif:UFA1, 2023 . - 1 vol (52 f .) ; 29cm.
Langues : Français (fre)
Catégories : Thèses & Mémoires:Informatique Mots-clés : E-learning
Plateforme d’apprentissageIndex. décimale : 004 Informatique Résumé : Les progrès des Technologies de l'Information et de la Communication (TIC) ont conduit à de nouveaux modes d’apprentissage, en particulier dans le domaine de l’éducation, tels que l’apprentissage à distance, également connu sous le nom d’apprentissage électronique. Cette approche implique l’utilisation de moyens de communication et de multimédia dans le processus éducatif. L’éducation à distance est devenue une solution fondamentale dans les cas où les restrictions de temps et d’espace sont problématiques ou impossibles, comme ce fut le cas avec la propagation de la pandémie de COVID-19.
Dans le cadre de ce projet, une plateforme d’apprentissage en ligne pour l’université de SETIF est développée sur la base du framework Laravel. Les étudiants et les enseignants peuvent s’inscrire à cette plateforme, où les enseignants peuvent afficher des cours et les étudiants peuvent les suivre. Les étudiants peuvent également évaluer leurs connaissances en posant des questions sur des informations incompréhensibles L’administrateur gère les différentes ressources de la plateforme ainsi que les et les droits d’accès des différents utilisateursCôte titre : MAI/0725 En ligne : https://drive.google.com/file/d/1bWs3pyQclSSUajYLkSmO-98tqhNza-sa/view?usp=drive [...] Format de la ressource électronique : Exemplaires (1)
Code-barres Cote Support Localisation Section Disponibilité MAI/0725 MAI/0725 Mémoire Bibliothéque des sciences Français Disponible
Disponible
