Vers Une Démarche Efficace De Traitement Du Model Checking Dans Les Cloud Computing

Résumé: Le Model checking a longtemps été utilisé comme moyen de vérification des spécifications formelles. C'est une technique de vérification qui explore tous les états possibles du système. Cette technique détermine si un système donné satisfait sa spécification. Cette technique souffre du problème d'explosion en temps et en espace mémoire. Dans cette thèse, nous avons proposé d'exploiter les ressources machines afin d'augmenter le gain en temps d'exécution en utilisant des algorithmes parallèles. Nous avons réalisé une comparaison entre deux approches parallèles et nous avons montré que notre approche était plus avantageuse en Model checking; Vérification formelle; Exploration; Algorithmes parallèles; Temps d'exécution; Algorithmes distribues; Espace mémoire; Spin; Gain en temps; Structures de données.temps d'exploration et en espace mémoire nécessaire pour le stockage des états. Nous avons par la suite effectué une comparaison entre une exploration parallèle et une exploration distribuée, nous avons conclu par une étude expérimentale, que l'approche parallèle affichait de meilleurs résultats et que le choix des structures de données était très important pour diminuer la complexité spatiale et temporelle d'un algorithme.

Publié dans la revue: