| Titre : | Evaluation de performance de protocoles dans l'internet des objets a base de methodes formelles |
| Auteurs : | Siham Benaoune, Auteur ; Laïd Kahloul, Directeur de thèse |
| Type de document : | Monographie imprimée |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2017 |
| Format : | 1 vol. (85 p.) / 30 cm |
| Langues: | Français |
| Mots-clés: | performance - protocoles -l'internet -objets - base - methodes formelles |
| Sommaire : |
Table des matières Remerciment……………………………………………………………………….. I Table des matières…………………………………………………………………. II Liste des figures……………………………………………………………………. V Liste des tableaux………………………………………………………………….. VII Introduction Générale……………………………………………………………… 1 Chapitre 1 - L’internet des objets 2 I-1 Introduction ……………………………………………………………………. 3 I-2 Avantages de l’Internet des Objets(IoT)……………………………………….. 3 I-3 Défis de l’Internet des Objets(IoT)……………………………………………… 3 I-4 Les Normes et la standardisation……………………………………………….. 7 I-5 Sécurité dans les protocoles IoT………………………………………………… 9 I-6 Protocoles de messagerie IoT……………………………………………………. 10 I-7 Conclusion ……………………………………………………………………… 12 Chapitre 2- l’analyse de performance des systèmes 13 II-1 Introduction …………………………………………………………………….. 14 II-2 Les performances des systèmes…………………………………………………. 14 II-2-1 Analyser les performances ……………………………………………………….. 14 II-2-1-1 L'expérimentation du système réel……………………………………………… 14 II-2-1-2 La modélisation………………………………………………………………….. 14 II-3 Vérification qualitative et analyse quantitative………………………………… 15 II-4 Techniques de modélisation…………………………………………………….. 16 II-4-1 La simulation à événements discrets…………………………………………… 16 II-4-2 Les méthodes analytiques ………………………………………………………. 16 II-4-3 Les méthodes formelles…………………………………………………………. 16 II-4-3-1 La construction assistée de preuves (theorem proving)……………………….. 17 II-4-3-2 La vérification de modèles (model checking)…………………………………. 17 II-5 Exigences de performance………………………………………………………. 18 II-5-1 L'accessibilité ……………………………………………………………………. 18 II-5-2 L'invariance de propriété ……………………………………………………….. 18 II-5-3 La sûreté…………………………………………………………………………… 18 II-5-4 La vivacité ………………………………………………………………………. 18 II-5-5 L'équité…………………………………………………………………………… 18 II-5-6 L'absence de blocage…………………………………………………………….. 18 II-6 Le model checking……………………………………………………………… 19 II-6-1 Le model checking classique……………………………………………………. 19 II-6-1-1 Les logiques temporelles (LTL – CTL – CTL*)………………………………… 19 II-6-2 Le model checking stochastique………………………………………………… 21 II-6-2-1 Notion de processus stochastique………………………………………………. 22 II-6-2-2 Chaînes de Markov à temps discret (DTMC)………………………………….. 22 II-6-2-3 Logique temporelles stochastiques (PCTL)……………………………………. 22 II-6-3 Le model checking temporisé…………………………………………………… 23 II-6-3-1 Logiques temporelles temporisées………………………………………………. 23 II-6-3-1-1 Extension temporisée de CTL ( La logique TCTL)……………………………. 23 II-6-3-1-2 Extension temporisée de LTL (La logique MTL)………………………………. 23 II-6-4 Model checking probabiliste et temporisé- logique temporelle PTCTL………. 23 II-7 Outils de Model Checking……………………………………………………… 24 II-7-1 PRISM…………………………………………………………………………… 24 II-7-2 FORTUNA……………………………………………………………………….. 24 II-7-3 UPPAAL…………………………………………………………………………… 24 [ III ] II-8 Conclusion……………………………………………………………………….. 25 Chapitre 3- Le protocole MQTT 26 III-1- Introduction …………………………………………………………………….. 27 III-2- Mode de fonctionnement ………………………………………………………. 28 III-2-1 Topologies MQTT………………………………………………………………. 28 III-2-2 Fonctionnement………………………………………………………………… 29 III-2-2-1 Connexion et Déconnexion…………………………………………………….. 29 III-2-2-2 Abonnements et Publications………………………………………………….. 30 III-2-3 Topic et motifs de filtrage ……………………………………………………… 30 III-2-4 Qualité de service ………………………………………………………………. 31 III-2-5 Dernière volonté et testament (Last Will & Testament)………………………. 33 III-2-6 Sécurité………………………………………………………………………….. 33 III-3 Description informelle du protocole……………………………………………. 34 III-3-1 Représentations de données………………………………………………………. 34 III-3-2 Structure d'un paquet de contrôle MQTT………………………………………. 34 III-3-2-1 Entête fixe………………………………………………………………………… 34 III-3-2-2 CONNECT…………………………………………………………………………. 36 III-3-.2-3 CONNACK ……………………………………………………………………… 41 III-3-2-4 PUBLISH ………………………………………………………………………… 42 III-3-2-5 PUBACK, PUBREC, PUBREL, PUBCOMP …………………………………… 43 III-3-2-6 SUBSCRIBE …………………………………………………………………….. 44 III-3-2-7 SUBACK…………………………………………………………………………. 45 III-3-2-8 UNSUBSCRIBE…………………………………………………………………. 46 III-3-2-9 UNSUBACK ……………………………………………………………………… 46 III-3-2-10 PINGREQ, PINGRESP……………………………………………………………. 46 III-3-2-11 DISCONNECT……………………………………………………………………. 47 III-3-3 La synchronisation des requêtes envoyées au broker…………………………. 47 III-3-4 L’identifiant de client MQTT…………………………………………………… 48 III-3-5 Callbacks…………………………………………………………………………. 49 III-4 Conclusion……………………………………………………………………….. 51 Chapitre 4-Contribution 52 IV-1 Introduction ………………………………………………………………………. 53 IV-2 Proposition d’un modèle d’étude……………………………………………….. 53 IV-3 Modélisation semi formelle du protocole MQTT………………………………. 55 IV-3-1 Diagramme de classe…………………………………………………………….. 55 IV-3-2 Diagramme de séquences du protocole…………………………………………… 56 IV-3-3 Le client MQTT………………………………………………………………….. 58 IV-3-4 Le broker MQTT………………………………………………………………… 59 IV-4 Modélisation formelle avec les automates temporisés…………………………. 59 IV-4-1 Modèle d’un broker dans la phase de publication côté Publisher…………….. 61 IV-4-2 Modèle d’un broker dans la phase de publication côté Subscriber……………. 62 IV-4-3 Modèle d’un Subscriber………………………………………………………….. 62 IV-4-4 Modèle d’un Publisher…………………………………………………………… 63 IV-4-5 Modèle de Souscription/ Désinscription…………………………………………… 64 IV-4-3 Modèle de la phase de connexion ………………………………………………. 64 IV-5 Vérification des propriétés qualitatives………………………………………….. 64 IV-5-1 Propriétés d’accessibilité………………………………………………………… 64 IV-5-2 Propriété de sureté……………………………………………………………….. 66 [ III ] IV-5-3 Propriété de vivacité………………………………………………………………. 66 IV-6 Vérification des propriétés qualitatives temporisées…………………..……….. 67 IV- 7 Modélisation formelle avec les automates temporisés probabilistes…………… 67 IV-7-1 Vérification des propriétés quantitatives……………………………………….. 68 IV-8 Conclusion ………………………………………………………………………. 72 Conclusion générale 73 |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| MINF/327 | Mémoire master | bibliothèque sciences exactes | Consultable |
