Vérification parallèle de systémes concurrents en utilisant le Graphe d'Observation Symbolique / Hiba Ouni ; sous la direction de Kais Klai et de Zouari Belhassen

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Catalogue Worldcat

Vérification de modèles (informatique)

Algorithmes d'approximation

Méthodes formelles (informatique)

Logique temporelle

Klai, Kais (1972-....) (Directeur de thèse / thesis advisor)

Belhassen, Zouari (Directeur de thèse / thesis advisor)

Petrucci, Laure (19..-....) (Président du jury de soutenance / praeses)

Duret-Lutz, Alexandre (1978-....) (Rapporteur de la thèse / thesis reporter)

Van de Pol , Jaco (Rapporteur de la thèse / thesis reporter)

Klaudel, Hanna (Membre du jury / opponent)

Abid, Chiheb Ameur (Membre du jury / opponent)

Université Paris 13 (Organisme de soutenance / degree-grantor)

Université de Tunis El Manar (Organisme de cotutelle / degree co-grantor)

École doctorale Galilée (Villetaneuse, Seine-Saint-Denis) (Ecole doctorale associée à la thèse / doctoral school)

Laboratoire informatique de Paris-Nord (Villetaneuse, Seine-Saint-Denis) (Laboratoire associé à la thèse / thesis associated laboratory)

Résumé / Abstract : 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.

Résumé / Abstract : 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.