| Titre : | vérificatioon probabiliste de protocoles dans les réseaux de capteur sans fil |
| Auteurs : | Mariem Saighi, Auteur ; Zohra Hamidi, 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. (53p.) / 30 cm |
| Langues: | Français |
| Mots-clés: | vérificatioon -protocoles -les réseaux -capteur -fil |
| Sommaire : |
Table des matières 1 Les Protocoles MAC dans RCSFs 8 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2 Les Réseaux de Capteurs Sans Fil (RCSF) . . . . . . . . . . . . . . . . . . . . . 9 1.2.1 Définition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2.2 Domaines d’applications des RCSF . . . . . . . . . . . . . . . . . . . . . 10 1.2.3 Facteurs et contraintes des RCSF . . . . . . . . . . . . . . . . . . . . . . 11 1.2.4 Architecture d’un capteur . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.3 Protocoles de communication . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.3.1 Protocole MAC (Media Access Control) . . . . . . . . . . . . . . . . . . 13 1.3.2 Protocole de routage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.3.3 Classification des protocoles de routage . . . . . . . . . . . . . . . . . . . 14 1.4 Les Protocoles de la couche MAC . . . . . . . . . . . . . . . . . . . . . . . . . . 15 1.4.1 Protocoles basés sur un séquencement temporel ( schedule-based protocols) . . . . . . . . . . . 15 1.4.2 Protocoles basés sur la contention (Contention-based Protocols) . . . . . 16 1.4.3 Protocoles hybrides . . . . . . . . . . . . 17 1.4.4 Récapitulatif des caractéristiques des protocoles . . . . . . . . . . . . . . 18 1.5 Protocole IEEE 802.11 . . . . . . . . . . . . . . . . . . 18 1.5.1 Mode PCF ( Point Coordination Function ) . . . . . . . . . . . . . . . . 19 1.5.2 Mode DCF ( Distributed Coordination Function ) . . . . . . . . . . . . 19 1.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2 Model checking statistique 21 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.2 Méthodes de vérification formelle . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.2.1 La construction assistée de preuves ou théorème proving . . . . . . . . . 22 2.2.2 La vérification de modèles ou model checking . . . . . . . . . . . . . . . 22 2.3 Formalismes de modélisation du mode checking . . . . . . . . . . . . . . . . . . 23 2.3.1 Les automates temporisés (Timed Automata :Ta) . . . . . . . . . . . . . 23 2.3.2 Automatestemporisésprobabilistes(ProbabilisticTimeAutomata:ProbTA . . .. . . . . . . . . . . . . 25 2.3.3 Automates temporisés à coût (Priced Timed Automata : PriceTA) . . . 26 2.4 Spécification des propriétés des systèmes . . . . . . . . . . . . . . . . . . . . . . 27 2.4.1 Logique temporelle : . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.4.2 Extension de la logique temporelle CTL . . . . . . . . . . . . . . . . . . 31 2.4.3 La logique TCTL (Timed Computation Tree Logic) . . . . . . . . . . . . 31 2.4.4 La logique PCTL ( Probabilistic Computation Tree Logic ) . . . . . . . . 32 2.5 Outils de model checking . . . . . . . . . . . . . . . . . . . . . . .. . . 34 2.5.1 SPIN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2.5.2 UPPAAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1 2.5.3 UPPAAL-SMC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.5.4 PRISM. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.5.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3 Conception et Implémentation 37 3.1 Introduction . . . . . . . . . . .. . . . . . . . . . . . . . . . . . 38 3.2 Description du protocole CSMA/CA . . . . . . . . . . . . . . . . . . . . . . . . 38 3.3 Algorithme de protocole CSMA/CA . . . . . . . . . . . . . . . . . . . . . . . . 38 3.4 Modélisation formelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 3.4.1 Modélisation formelle avec les automates temporisés probabilistes . . . . 40 3.5 PRISM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.6 Les modèles avec PRISM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.6.1 Module station . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.6.2 Module backoff . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 3.6.3 Module medium . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3.7 Vérification avec PRISM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 3.8 Les propriétés vérifiées . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 3.8.1 Vérification des propriétés quantitative . . . . . . . . . . . . . . . . . . . 49 3.8.2 Vérification des propriétés quantitative temporisées . . . . . . . . . . . . 50 3.9 La conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| MINF/306 | Mémoire master | bibliothèque sciences exactes | Consultable |
