La logique temporelle linéaire (LTL)

Table des matières

RÉSUMÉ
REMERCIEMENTS
TABLE DES MATIÈRES
LISTE DES TABLEAUX
LISTE DES FIGURES
CHAPITRE 1 INTRODUCTION
CHAPITRE 2 REVUE DE LITTÉRATURE
2.2 La logique temporelle linéaire (LTL)
2.2.1 Trace d’événements
2.2.2 LTL
2.2.3 Opérateurs Temporels
2.2.3.1 Opérateur G
2.2.3.2 Opérateur F
2.2.3.3 Opérateur U
2.2.3.4 Opérateur X
2.2.4 Syntaxe et Sémantique formelle de la LTL
2.3 Les outils séquentiels
2.3.1 BeepBeep
2.3.2 Logscope
2.3.3 Maude
2.3.4 Monid
2.3.5 MonPoly
2.3.6 ProM
2.3.7 RuleR
2.3.8 Saxon
2.3.9 SEQ. OPEN
2.3.10 Résumé
CHAPITRE 3 MAPREDUCE
3.1 Description des composants de MapReduce
3.1.1 L’InputReader
3.1.2 Mapper
3.1.3 Shuffling
3.1.4 Reducer
3.1.5 OutputWriter
3.2 Exemple de tâche
3.2.1 Mapper
3.2.2 Reducer
3.2.3 Objet de la tâche
3.2.4 Exécution de la tâche
3.3 Environnements MapReduce
3.3.1 Mr Sim
3.3.1.1 WordCount de Mr. Sim
Figure 5 : Tâche Mr Sim WordCount
3.3.2 Hadoop
3.3.2.1 WordCount de mode Hadoop
3.3.3 Mr Sim VS Hadoop
CHAPITRE 4 LTL APPLIQUÉE AU MAPREDUCE
4.2. Format de la trace et l’InputReader
4.3 Mapper
4.4 Reducer
4.5 OutputWriter
4.6 Exemple
4.7 LTL-Past
4.7.1 Les ajouts
4.7.1.1 Opérateur S
4.7.1.2 Opérateur H
4.7.1.3 Opérateur O
4.7.1.4 Opérateur Y
4.7.2 Les impacts
CHAPITRE 5 IMPLÉMENTATION DANS MR. SIM
5.1 LTLValidator
5.1.1 Formules LTL
5.1.2 LTLTuple
5.1.3 Phase lecture
5.1.4 Mr Sim parallèle
5.2 Outils connexes
5.2.1 XMLTraceGenerator
5.2.2 TagCounter
5.2.3 JobLauncher
CHAPITRE 6 IMPLÉMENTATION DANS HADOOP
6.1 Environnement de développement
6.2 Structure XML
6.3 Format d’entrée de Hadoop
6.3.1 FileInputFormat
6.3.2 LTLInputFormat1Gen
6.3.3 LTLInputFormatXGen
6.4 Format des objets de transitions
6.4.1 Writable
6.4.2 WritableComparable
6.5 Format de sortie
6.5.1 LTLOutputFormatXGen
6.5.2 LTLOutputFormatLastGen
6.6 Instanciation de la tâche
6.6.1 L’objet jobConf
6.6.2 Les formats de sortie
CHAPITRE 7 CLUSTER HADOOP MAPREDUCE
7.2 L’univers VMware
7.2.1 Project Serengeti
7.2.2 VMware VSphere
7.2.3 VMware VCenter Server
7.2.4 Windows Server 2008
7.2.5 Le déploiement du cluster
7.3 L’univers Solaris
7.3.1 Oracle Solaris 11.1
7.3.2 Oracle VM VirtualBox
7.3.3 Observation sur le tutoriel
7.3.4 Exécution de tâche sur un cluster
CHAPITRE 8 TESTS DE PERFORMANCE ET COMPARAISONS
8.1 Environnement d’exécution
8.2 Les environnements de tests
8.2.1 Mr Sim
8.2.2 Hadoop
8.3 Formules LTL
8.4 Résultats
8.4.1 Nombre de tuples
8.4.2 Temps d’exécution
CONCLUSION
BIBLIOGRAPHIE
ANNEXE 1
ANNEXE 2
ANNEXE 3
ANNEXE 4
ANNEXE 5