Constellation, le dépôt institutionnel de l'Université du Québec à Chicoutimi

Résumé

Dans le présent mémoire nous aborderons la vérification de propriétés LTL dans un environnement Hadoop MapReduce. Nous allons en premier parler de l’utilité d’une telle idée. Donc, nous allons définir notre source de données. Ensuite, nous définirons pourquoi ce type d’analyse est intéressant et ensuite les outils existants. Par la suite, nous allons nous pencher sur la logique utilisée pour permettre d’écrire les faits ou informations à observer sur les données d’analyse. La logique utilisée est la logique temporelle linéaire et nous prendrons le temps de définir ce que sont les opérateurs contenus dans cette dernière. Sans oublier, nous parlerons de la structure des données utilisées et les avantages de cette dernière. Nous étudierons le paradigme MapReduce qui permet d’encadrer le traitement selon une structure prédéfinie. Donc, nous allons présenter l’ensemble des phases avec une description permettant de bien identifier leur utilité. Ensuite, nous introduirons les outils permettant d’utiliser le paradigme MapReduce. C’est-à-dire de ce que sont Mr Sim et l’environnement Hadoop MapReduce. Nous allons décrire le fonctionnement distribué de ces environnements à travers les différentes phases. De plus, pour permettre de mieux comprendre ces environnements, nous présenterons des explications en profondeur sur des exemples concrets. Pour terminer, nous effectuerons une comparaison entre les deux outils. Ensuite, nous parlerons de l’implémentation des différentes phases du paradigme MapReduce selon nos besoins. Nous présenterons des pseudo-codes pour l’ensemble des phases accompagnés d’explication pour bien saisir les nuances dans la logique. Nous terminerons par présenter un exemple complet émulant le traitement des différentes phases. Nous continuerons par présenter l’implantation de l’algorithme dans les différents environnements MapReduce. C’est-à-dire que nous présenterons l’ensemble des objets nécessaires permettant de donner vie à notre algorithme d’analyse. Sans oublier de présenter les particularités propres et incontournables que nécessite chaque environnement. Par la suite, nous présenterons les possibilités existantes pour créer un cluster MapReduce. Soit dans deux univers différents, dans deux configurations distinctes. Finalement, nous conclurons en présentant des tests de performance effectués dans nos environnements de références. Pour ce faire, nous présenterons les propriétés étudiées et les sources de données analysées.