Domaines d'application du Model checking

Domaines d’application du Model checking

Model checking et exploration

Le Model checking est une technique de vérication, basée sur l’exhaustivité et l’exploration de l’espace des états des systèmes, dans la recherche de comportements qui ne vérient pas leurs spécications. Un véricateur de modèles peut être considéré comme une boîte noire, qui accepte comme entrée un système ainsi qu’une propriété exprimée sur ce système et renvoie une réponse, indiquant si la propriété est vériée ou non. Lors de la vérication des propriétés, tous les comportements possibles du système sont énumérés et les propriétés sont vériées. Les algorithmes mis en ÷uvre comprennent deux phases, une construction de l’espace d’états puis une exploration de cet espace d’états dans la recherche d’erreurs. L’espace d’états est représenté comme un graphe qui décrit toutes les évolutions possibles du système. Les n÷uds du graphe représentent les états du système et les arcs représentent les transitions entre ces états [2, 3]. L’analyse de l’accessibilité consiste à explorer les modèles état par état, chaque état et tous ses successeurs sont stockés en mémoire. L’exploration se termine lorsque tous les états sont visités. Un algorithme d’exploration, à chaque étape de son exécution, peut soit visiter un nouveau n÷ud, soit un n÷ud exploré.

ETAT DE L’ART

Nous allons présenter une solution basée sur une exploration parallèle, visant à obtenir une meilleure exploration en temps sur l’outil Spin. Les autres solutions ont été proposées pour le problème d’explosion de l’espace d’états. Ces approches sont exécutées sur des architectures distribuées, parallèles ou séquentielles. Chacune d’elles est basée sur des structures de données diérentes.

Architecture séquentielle

Un algorithme correspond à une succession d’états et à des transitions entre ces états. L’idée est que les états correspondent à des descriptions instantanées de l’algorithme. Un algorithme d’exploration est déni principalement par trois paramètres : un critère d’arrêt de l’exploration, une fonction de sélection des états successeurs, à partir d’un état ou d’un ensemble d’états déjà explorés et stockés en mémoire, et une fonction qui permet d’eectuer le stockage de nouveaux états en mémoire. L’exécution de deux séquences est dite séquentielle lorsqu’elles sont exécutées l’une à la suite de l’autre. Dans une approche séquentielle, l’exploration est eectuée par un seul processus, le temps d’exploration peut être énorme si le nombre d’états est très élevé. Dans une exploration séquentielle, les états sont visités l’un à la suite de l’autre, le premier état visité est l’état initial, par la suite, les successeurs de cet état sont générés, puis stockés en mémoire. Ce processus s’arrête lorsque tous les états sont traités. L’approche proposée dans [ 62] est basée sur une représentation symbolique des états. Ces derniers sont stockés dans une structure OBDD (ObjectBinaryDecisionDiagram,quiestun arbre acyclique représentant des fonctions booléennes. C’est une forme réduite des diagrammes BDD [ 42] (voir chapitre 2 section 2.8.2 ). Pour chaque état exploré, un arbre OBDD lui est généré. Cela permet de stocker les états explorés. Les parties gauches de l’arbre représentent la valeur booléenne 0, et les parties droites la valeur 1. Les diagrammes OBDD peuvent être directement manipulés pour eectuer ecacement toutes les opérations booléennes de base [ 45]. Si un état s est exploré, il peut être représenté par une fonction booléenne f(s) = 1. La Figure. 3.2 présente un arbre de décision binaire composé de 3 états, représentant la fonction f(x1,x2,x3) = ¯ x1. ¯ x2. ¯ x3 + ¯ x1.x2. ¯ x3 +x1. ¯ x2. ¯ x3.

Architecture parallèle

Le parallélisme consiste à mettre en ÷uvre des architectures permettant de traiter des informations de manière simultanée. Dans ce qui suit, nous présentons 2 solutions au probléme d’explosion dans un environnement parallèle, la première pour gérer la complexité spatiale et la seconde prend en compte la complexité temporelle de l’algorithme d’exploration. La première solution a été étudiée dans [ 57]. Comme pour les 2 approches séquentielles précédentes (voir section 3.4.1 ) utilisant des structures de données visant à augmenter le plus possible le gain en espace mémoire. La solution décrite en détail dans [ 57] se base sur l’utilisation d’arbres AVL [ 2]. Le nom AVL provient de ceux qui ont créé cette structure. Ceux sont des arbres binaires de recherche. Les auteurs ont proposé un algorithme d’exploration appelé general lock free , exécuté dans une architecture parallèle à mémoire partagée. L’espace d’états est partagé par les processeurs et l’accès à cette dernière se fait en exclusion mutuelle. L’algorithme présenté par les auteurs est basé sur 2 structures de données, un ltre de bloom (structure de données probabiliste) [ 57], partagé entre les diérents processeurs pour indiquer si un état a été visité ou pas, ainsi que des piles privées et publiques. Chaque processeur gère une pile privée contenant les états qui doivent être explorés et une pile partagée contenant les états partagés par les processeurs (voir Figure. 3.4 ). Le ltre de bloom a été utilisé, car il est rapide en temps d’exécution et compacte en mémoire. Lorsqu’un état est généré, un test est réalisé sur cet état an de vérier s’il est ancien ou nouveau. Cette information est donnée par le ltre de bloom . Dans le cas où l’état est nouveau, il est stocké dans un arbre binaire. Dans certains cas, le ltre de bloom peut rendre un résultat positif alors que l’état n’a pas encore été vu. Cela est appelé un faux positif. Cette situation où des états sont supposés être traités alors qu’ils ne le sont pas, est appelée collision d’états. Ces états sont stockés dans un arbre binaire réservé aux collisions. L’algorithme est réparti en trois phases, exploration, collision et terminaison.

Le rapport de stage ou le pfe est un document d’analyse, de synthèse et d’évaluation de votre apprentissage, c’est pour cela rapport-gratuit.com propose le téléchargement des modèles complet de projet de fin d’étude, rapport de stage, mémoire, pfe, thèse, pour connaître la méthodologie à avoir et savoir comment construire les parties d’un projet de fin d’étude.

Table des matières

Table des figures
List of Figures
Liste des tableaux
List of Tables
1 Introduction générale
1.1 Contexte de travail
1.2 Solutions proposées
1.3 Expérimentations et évaluation des résultats
1.4 Organisation de la thèse
2 Model checking
2.1 Introduction
2.2 Vérication formelle
2.2.1 Simulation
2.2.2 Test
2.3 Model checking
2.4 Domaines d’application du Model checking
2.5 Logique temporelle
2.6 Avantages et inconvénients
2.7 Processus d’exécution du Model checking
2.8 Obstacle au Model checking : Explosion en temps ou en espace mémoire
2.8.1 Model checking à la volée
2.8.2 Représentation symbolique
2.8.3 Réduction
2.8.4 Raisonnement compositionnel
2.9 Quelques Model checkers
2.9.1 SPIN
2.9.2 SMV
2.9.3 NuSMV
2.9.4 KRONOS
2.9.5 UPPAAL
2.9.6 DIVINE
2.9.7 OBP
2.10 Conclusion
3 Explosion en temps et en espace mémoire : Etat de l’art
3.1 Introduction
3.2 Dénition du problème
3.3 Model checking et exploration
3.4 Etat de l’art
3.4.1 Architecture séquentielle
3.4.2 Architecture parallèle
3.4.3 Architecture distribuée
3.5 Conclusion
4 Contributions
4.1 Introduction
4.2 Objectifs
4.3 Exploration et graphe d’états
4.4 Contributions
4.4.1 Première contribution
4.4.2 Seconde contribution : Algorithme SPA
4.4.3 Comparaison entre les deux approches parallèles
5 Expérimentations
5.1 Introduction
5.2 Environnement de développement
5.3 Etude expérimentale
5.4 Espace mémoire utilisé à l’étape d’exploration
5.5 Conclusion
6 Conclusion générale
Bibliographie