Vérification parallèle de systémes concurrents en utilisant le Graphe d’Observation Symbolique - Laboratoire d'Informatique de Paris-Nord Accéder directement au contenu
Thèse Année : 2019

Parallel verification of concurrent systems using the Symbolic Observation Graph

Vérification parallèle de systémes concurrents en utilisant le Graphe d’Observation Symbolique

Résumé

The model checking is one of the major techniques used in the formal verification. Thistechnique takes a model of a system in question and decides whether it satisfies a givenproperty or not. It is based on an exhaustive exploration of the state space of the systemto be verified. Thus, the Model checking technique suffers from the state space explosionproblem. It can happen that the verification process stops because of lack of memoryspace. One solution is to reduce state space representation by using a symbolicrepresentation such as symbolic observation graphs. Using symbolic graphs requiresmore intensive computations that induces a drastic increase in runtime. In order to reduceruntime, we propose to parallelize the verification process. The use of distributedprocessing increases the speedup and scalability of model checking by exploiting thecumulative computational power and memory of a cluster of computers. Such approacheshave been studied in various contexts leading to different proposed solutions for bothsymbolic and explicit model checking. In this thesis, we propose a new model checkingalgorithms built on a parallel construction of the Symbolic Observation Graph: anabstraction of the state space graph that preserves Linear Temporal Logic (LTL). Weimplemented the proposed model checking algorithms within a C++ prototype andcompared our preliminary results with the state of the art model checkers.
Le Model Checking est l'un des techniques principales utilisées dans la vérificationformelle. Cette technique prend un modèle du système en question et décide s'ilsatisfait ou non une propriété donnée. Il est basé sur une exploration exhaustive del'espace d'états du système à vérifier. Malgré son efficacité et sa simplicité, une telledémarche se heurte au problème d'explosion combinatoire de l'espace d'états. Il peutarriver que le processus de vérification s’arrête par manque d’espace mémoire. Unesolution consiste à réduire la représentation d'espace d'états en utilisant unereprésentation symbolique telle que des graphes d'observation symboliques.L'utilisation de graphes symboliques nécessite des calculs plus intensifs qui induisentune augmentation considérable du temps d'exécution. Afin de réduire le tempsd’exécution, nous proposons de paralléliser le processus de vérification. L'utilisationdu traitement distribué augmente la rapidité et l'évolutivité de la vérification dumodèle en exploitant la puissance de calcul cumulative et la mémoire d'un clusterd'ordinateurs. Telles approches ont été étudiées dans divers contextes, ce qui aconduit à différentes solutions proposées pour le Model Checking à la foissymbolique et explicite. Dans cette thèse, nous proposons un nouvel algorithme deModel Checking basé sur une construction parallèle du graphe d’observationsymbolique: une abstraction de l’espace d’états préservant la logique temporellelinéaire (LTL). Nous avons implémenté les algorithmes proposés dans un prototypeC ++ et comparé nos résultats préliminaires aux Model Checkers de l'état de l'art.
Fichier principal
Vignette du fichier
edgalilee_th_2019_ouni.pdf (684.4 Ko) Télécharger le fichier
Origine : Version validée par le jury (STAR)

Dates et versions

tel-03340239 , version 1 (10-09-2021)

Identifiants

  • HAL Id : tel-03340239 , version 1

Citer

Hiba Ouni. Vérification parallèle de systémes concurrents en utilisant le Graphe d’Observation Symbolique. Modélisation et simulation. Université Paris-Nord - Paris XIII; Université de Tunis El Manar, 2019. Français. ⟨NNT : 2019PA131092⟩. ⟨tel-03340239⟩
79 Consultations
61 Téléchargements

Partager

Gmail Facebook X LinkedIn More