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

Vérification de propriétés LTL dans un environnement Hadoop MapReduce

Soucy-Boivin Maxime. (2015). Vérification de propriétés LTL dans un environnement Hadoop MapReduce. Mémoire de maîtrise, Université du Québec à Chicoutimi.

[thumbnail of SoucyBoivin_uqac_0862N_10115.pdf] PDF
1MB

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.

Type de document:Thèse ou mémoire de l'UQAC (Mémoire de maîtrise)
Date:Avril 2015
Lieu de publication:Chicoutimi
Programme d'étude:Maîtrise en informatique
Nombre de pages:135
ISBN:Non spécifié
Sujets:Sciences naturelles et génie > Sciences mathématiques > Informatique
Département, module, service et unité de recherche:Départements et modules > Département d'informatique et de mathématique > Programmes d'études de cycles supérieurs en informatique
Directeur(s), Co-directeur(s) et responsable(s):Hallé, Sylvain
Mots-clés:analyse de logs, Hadoop, LTL, MapReduce, traitement parallèle
Déposé le:10 févr. 2016 16:22
Dernière modification:11 févr. 2016 23:17
Afficher les statistiques de telechargements

Éditer le document (administrateurs uniquement)

Creative Commons LicenseSauf indication contraire, les documents archivés dans Constellation sont rendus disponibles selon les termes de la licence Creative Commons "Paternité, pas d'utilisation commerciale, pas de modification" 2.5 Canada.

Bibliothèque Paul-Émile-Boulet, UQAC
555, boulevard de l'Université
Chicoutimi (Québec)  CANADA G7H 2B1
418 545-5011, poste 5630