Informations
Directeur de thèse :
Année de début :
Fin 2010
Université :
Université Constantine 2
Soutenance
Date de soutenance :
22 Mars 2018
Jury :
Salim Chikhi
Djamel Eddine Saidouni
Fateh Boutekkouk
Makhlouf Derdour
Nadia Zeghib
Manuscrit
Téléchargement :
Détails
Titre :
Proposition d’algorithmes de distribution des espaces d’états en vue d’une vérification basée model checking : Application aux automates temporisés avec durées d’actions

Résumé :

La vérification formelle constitue une étape indispensable pour garantir le bon fonctionnement des systèmes complexes et critiques. L’une des techniques les plus répandues est le model checking qui se base sur l’exploration exhaustive de l’espace d’états, ce qui mène à un problème majeur : L’explosion combinatoire liée aux espaces d’états des systèmes même de taille réaliste.

Nous nous attachons, dans ce travail de thèse, à combattre ce problème par la proposition de solutions qui s’appuient sur la distribution de la génération de l’espace d’états sur un réseau de machines connectées afin de tirer profit de la quantité de mémoire et de la puissance de calcul disponibles. L’aspect novateur de nos approches est la définition du problème de génération parallèle de l’espace d’états comme un problème d’optimisation et l’utilisation des méthodes d’optimisation pour optimiser la distribution des états.

Pour cela, nous proposons deux algorithmes ; le premier est une adaptation d’un algorithme d’optimisation par colonie de fourmis inspiré du comportement de tri du couvain par les fourmis réelles. Tandis que le deuxième se base sur le modèle parallèle de l’algorithme génétique, où plusieurs processus de recherche indépendants sur des différentes sous-populations évoluent en parallèle afin de construire une bonne distribution de l’espace d’états.

De plus, nous proposons une nouvelle politique de distribution basée sur l’analyse du comportement des systèmes analysés et dont la distribution est optimisée et guidée par le système à chaque fois qu’une vérification est lancée sur le modèle associé à ce système.

Les résultats obtenus sont très encourageants et montrent l’efficacité de nos approches dans la mesure où elles prennent en considération les deux aspects essentiels des applications distribuées à savoir l’équilibrage de la charge et du travail ainsi que la minimisation du coût de communication induit par le nombre des transitions liant des états stockés sur des machines différentes.


Mots clés :
Model checking Explosion combinatoire Systèmes temps réels Calcul parallèle Génération de l’espace d’états Méthodes d’optimisation Heuristiques


Abstract:

Formal verification is an essential step for ensuring the proper functioning of complex and critical systems. One of the most widely used approach is the Model checking, which is based on the exhaustive exploration of the state space. This latter leads to a major problem: the combinatorial explosion of the state spaces of the realistic systems.

In the scope of this thesis, we contribute for solving this problem by proposing solutions based on the distribution of the state space generation upon a network of connected machines. This proposition aims at exploiting both the memory quantity and the computation power. The innovative aspect of our proposed approaches is the definition of the parallel generation of the state space as an optimization problem and using the optimization methods in order to optimize the states’ distribution.

For this, we propose two algorithms; the first constitutes an adaptation of an ant colony optimization algorithm inspired by the brood sorting behavior of the real ants. While the second is based on a parallel model of the genetic algorithm, where many independent search processes on different sub-populations evolve in parallel in order to construct a good state space distribution.

In addition, we propose a new distribution policy based on analyzing the behavior of the analyzed systems and whose distribution is optimized and guided by the system whenever the system verification is launched.

The obtained results are very promising, and they show the effectiveness of the proposed approachesintheopticwherethesemethodstakeintoconsiderationthetwoimportantaspectsof the distributed applications; the workload balancing and the minimization of the communication cost caused by the transitions between states located in different machines.


Keywords:
Model checking Combinatorial explosion Real-time systems Parallel computation State space generation Optimization methods Heuristics