| Titre : | Intégration des méthodes formelles dans le développement des RCSFs |
| Auteurs : | Zohra Hmidi, Auteur ; Saber Benharzallah, Directeur de thèse ; Laïd Kahloul, Directeur de thèse |
| Type de document : | Thése doctorat |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2023 |
| Format : | 1 vol. (99p.) / ill., couv. ill. en coul / 30cm |
| Langues: | Anglais |
| Résumé : |
In this thesis, we have relied on formal techniques in order to first evaluate WSN protocols and then to propose solutions that meet the requirements of these networks. The thesis contributes to the modelling, analysis, design and evaluation of WSN protocols. In this context, the thesis begins with a survey on WSN and formal verification techniques. Focusing on the MAC layer, the thesis reviews proposed MAC protocols for WSN as well as their design challenges. The dissertation then proceeds to outline the contributions of this work. As a first proposal, we develop a stochastic generic model of the 802.11 MAC protocol for an arbitrary network topology and then perform probabilistic evaluation of the protocol using statistical model checking. Considering an alternative power source to operate WSN, energy harvesting, we move to the second proposal where a protocol designed for EH-WSN is modelled and various performance parameters are evaluated. Finally, the thesis explores mobility in WSN and proposes a new MAC protocol, named "Mobility and Energy Harvesting aware Medium Access Control (MEH-MAC)" protocol for dynamic sensor networks powered by ambient energy. The protocol is modelled and verified under several features. Key words: Wireless Sensor Networks, Medium Access Control, Formal Modelling, Formal Verification, Statistical Model Checking, Stochastic Timed Automata, Energy Harvesting, Mobility. |
| Sommaire : |
General Introduction 1 1 Specification and Verification of Wireless Sensor Networks 5 1.1 Introduction . . . . . . . 6 1.2 An overview of WSN . . . . . . . . . . 6 1.2.1 Definition . . . . . . . . . . . . . 6 1.2.2 Constraints and Requirements . . . . . . . 7 1.2.3 Types of Wireless Sensor Networks . . . . . 8 1.2.4 Applications . . . . . . 9 1.2.5 Communication Protocols for WSN . . .. . 10 1.2.6 Cross Layer Approach . . . . . . . . . . . 11 1.3 WSN Protocol Verification Methods . . . . . . .. . . . 11 1.3.1 Formal Verification Methods . . . . . . . 12 1.3.2 Formal Modelling Languages . . . . . . .. . 15 1.3.3 Properties Specification Formalisms . . . . . . 19 1.4 Conclusion . . . . . . . 23 2 MAC Protocols for Wireless Sensor Networks 24 2.1 Introduction . . . . . . . . . . 25 2.2 Communication Patterns . . . . . . . . . . . 25 2.3 MAC Protocol Design Challenges . . . . . . 26 2.3.1 Energy Consumption Sources . . . . . .. 26 2.3.2 Power Saving Modes of Operation . . . . 26 2.3.3 Error Detection . . . . . . . . . . . . . . . . . . 27 2.4 Performance Metrics for MAC Protocols . . . . . . . . 29 2.5 Classification of MAC Protocols for WSN . . . . . . . . 29 2.5.1 Contention-based Protocols . . . . . . . . . 29 2.5.2 Schedule-based Protocols . . . . . . . . . . . 32 2.5.3 Hybrid Protocols . . . . . . . 34 2.6 Comparison of MAC Protocols . . . . . . . 37 2.7 Cross-layer Approaches . . . . . . . . . . . . 38 2.7.1 MAC-CROSS protocol . . . . . . . . . 39 2.7.2 XLM Protocol . . . . . . . . . . 40 2.7.3 EYES MAC Protocol . . . . . 40 2.8 Energy Harvesting MAC Protocols . . . . . . . . . . . . . . . 41 2.8.1 Probabilistic Polling for Single-hop WSNs . . . 41 2.8.2 EH-MAC Probabilistic Polling for Multi-hop WSNs . . . . 42 2.8.3 Multi-Tier Probabilistic Polling (MTPP) . . . . 42 2.9 Conclusion . . . . . . 43 3 Stochastic Generic Model for 802.11 Basic Access MAC Protocol 45 3.1 Introduction . . . . . . . . . . 46 3.2 Informal Description . . . . . .. . . . 46 3.3 Formal Tools . . . . . . . . . . . . . . . . . . . . . 48 3.3.1 Statistical Model Checking . . . . . . . . . . 48 3.3.2 Query Language . . . . . . . . . . . . . . . 48 3.4 Stochastic Models of the Protocol . . . . . . . 49 3.5 Protocol Analysis . . . . . . . . . . . . . . . . . . .. . . . 51 3.5.1 Verification of Qualitative Properties . . . . . 52 3.5.2 Verification of Quantitative Properties . . . . . .. 52 3.6 Comparison . . . . . . . . . . . . . . . . . . . 55 3.7 Conclusion . . . . . . . . . . . 56 4 Performance Evaluation of ODMAC Protocol for WSNs Powered by Ambient Energy 57 4.1 Introduction . . . . . . . . 58 4.2 Related Work . . . . . . . . . . . . . . . . . . . . . 58 4.3 Basic MAC Schemes Evaluation . . . . . . . . . . . . . . 59 4.4 On Demand Medium Access Control (ODMAC) . . . . .. 60 4.5 Performance Metrics . . . . . . . . . .. . . . 62 4.5.1 Delay and Throughput . . . 62 4.5.2 Power Consumption . . . . . . . . . . . . . . 63 4.6 Modelling ODMAC using Timed Automata . . . . . . . 63 4.7 Analysis using UPPAAL-SMC . . . . . . . . . . . . . . 66 4.7.1 Static Duty Cycle . . . . . . . . . . 67 4.7.2 Dynamic Duty Cycle . . . . . . . . . . . . . . 68 4.7.3 Variable Harvesting Rate . . . . . . 71 4.8 Conclusion . . . . . . . . . . . . . . . . . . 73 5 A new Mobility and Energy Harvesting aware Medium Access Control (MEHMAC) Protocol: Modelling and Performance Evaluation 74 5.1 Introduction . . .. . . . 75 5.2 Related Work . . . . . . . . 75 5.3 MEH-MAC Description . . . . . . . . . . . . . . 76 5.3.1 Static Communication . . . . . . . 77 5.3.2 Dynamic Communication . . . . . . .. 79 5.3.3 Energy-neutral Operation State . . . . . . . . . 83 5.3.4 Doppler Effect Formulation . . . . . . . . . .84 5.3.5 Hand-off Handling . . . . . . . . . . .. . 85 5.4 MEH-MAC Modelling . . . . . . . . . . .. . 86 5.5 Case Study for the Analysis Phase . . . . . . . . 90 5.6 Analysis and Evaluation . . . . . . . . . . 91 5.6.1 ODMAC Evaluation . . . . . . . . .. 92 5.6.2 MEH-MAC Evaluation . . . . . . . 93 5.6.3 ENO State Evaluation . . . . . . . . . 94 5.6.4 Packet Error Evaluation . . . . . . . . . 95 5.6.5 Hand-off Evaluation . . . . . . . . . . . . . . 96 vCONTENTS 5.7 Comparison with Recent Works . . . . . 97 5.8 Conclusion . . . . . . 97 General Conclusion 99 |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| TINF/189 | Théses de doctorat | bibliothèque sciences exactes | Consultable |
