| Titre : | Transformation du problème de model-checking vers un problème de satisfiabilité |
| Auteurs : | Mohamed Salah Guedjiba, Auteur ; Zohra Hamidi, Directeur de thèse |
| Type de document : | Monographie imprimée |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2017 |
| Format : | 1 vol. (43 p.) / 30 cm |
| Langues: | Français |
| Mots-clés: | Model-checking,model cheking symbolique,vérification formelle,structure de Kripke,arbre de décision binaire réduit et ordonné,la logique CTL. |
| Résumé : |
Model checking est une méthode de vérification formelle automatique. Le système étudié est décrit sous forme de modèle à états-transitions qui représente sa spécification. A partir de ce premier modèle est généré un second modèle qui est une interprétation sémantique du premier et qui représente tous les comportements possibles du système. Des algorithmes permettent d’explorer exhaustivement de l’espace d’états des comportements. Durant cette exploration, l’algorithme de model-checking vérifie certains types de propriétés. Ces propriétés sont généralement représentés avec la logique CTL, la recherche exhaustive rend l’algorithme du model-checking très coûteux. L’objectif de ce travail est de rendre ce problème un problème de satisfiabilité c.à.d. d’essayer de représenter le système étudié (automate de kripke + la formule CTL) sous forme d’une formule de la logique propositionnelle. Ensuite, de la représenter sous forme d’arbre BDD et enfin de vérifier sa satisfiabilité. |
| Sommaire : |
Introduction générale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1 Model-checking 9 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2 Model-checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2.1 Définition du model-checking . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2.2 Principe du model-checking . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.2.3 Objectif du model-checking . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.2.4 Limitation du model checking . . . . . . . . . . . . . . . . . . . . . . . . 12 1.3 Model-checking symbolique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.4 Les structures de Kripke . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.5 Logique CTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 1.5.1 Présentation du langage CTL . . . . . . . . . . . . . . . . . . . . . . . . 15 1.5.2 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.5.3 Sémantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2 Vérification symbolique des formules CTL en utilisant les BDDs 20 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.2 Arbre de décision binaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.3 Diagramme de décision binaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.4 Quelques avantages de BDD . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.5 Diagramme de décision binaire ordonné(OBDD) . . . . . . . . . . . . . . . . . . 28 2.6 Diagramme de décision binaire ordonné et réduit(ROBDD) . . . . . . . . . . . . 28 2.7 Vérification symbolique des formules CTL . . . . . . . . . . . . . . . . . . . . . 30 2.7.1 Représentation des états . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.7.2 Représentation de relation de transition . . . . . . . . . . . . . . . . . . . 31 2.7.3 Formule CTL vers BDD . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3 Conception et réalisation d’un outil du model checking symbolique 37 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.2 L’architecture générale du système . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.3 Le diagramme de séquence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.4 Le diagramme d’activité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.5 Implémentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.5.1 Éditeur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.5.2 Transformateur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.5.3 Représentation symbolique . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.5.4 Vérificateur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 3.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Conclusion générale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Bibliographie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| MINF/295 | Mémoire master | bibliothèque sciences exactes | Consultable |
