| Titre : | Modelling, verification and performance evaluation of the CSMA/CA protocol in WSNs, by Coloured Petri Nets |
| Auteurs : | SIHAM ZROUG, Auteur |
| 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, 2021 |
| Langues: | Français |
| Mots-clés: | Medium Access Control, Wireless Sensor Networks, CSMA/CA, EHWSNs,Formal Modelling, Formal Analysing, Performance Evaluation, Coloured Petri nets, Linear Temporal Logic. Machine Learning |
| Résumé : |
This thesis tackles the problem of formal modelling and verification of Carrier Sense Multiple Access with Collision Avoidance (CSMA/CA) protocol in wireless sensor networks. Indeed, our research focuses on the modelling, the verification and performance evaluation of CSMA/CA using Coloured Petri Nets (CPNs). Medium Access Control (MAC) protocol plays a vital role in performance of wireless sensor networks due to its crucial purpose to emulate successful communication. The CSMA/CA protocol was one of the predominant protocols in WSNs for its contention mechanism and channel access. This thesis provides three basic contributions. In the first contribution, Hierarchical Timed Coloured Petri Nets (HTCPNs) formalism is used to model the CSMA/CA protocol, and then the CPN-Tools is exploited to analyse the obtained models. Indeed, the timed aspect in HTCPN allows us to deal with temporal constraints in CSMA/CA. The hierarchical aspect of HTCPN makes the CSMA/CA model "manageable", despite the complexity of the protocol. The limited energy associated with WSNs is a major drawback of WSN technologies. To overcome this major limitation, the design and development of efficient and high performance energy harvesting (EH) systems for WSNs environments are being explored. Hence, as a second contribution, a hierarchical timed coloured Petri net model for CSMA/CA in EH-WSNs is proposed. In order to evaluate the proposed model, a set of qualitative and quantitative properties are verified. Linear Temporal Logic (LTL) is used to formalise and verify qualitative properties. The quantitative verification is done by using extracted files from monitors results defined in CPN-Tools. As a third contribution, a Machine Learning (ML) is used to discuss the scalability of the first proposed model when the number of sensor nodes is increased. An effective neuronal network is exploited for the prediction of the throughput metric of the network based on the number of nodes to prove the scalability of the proposed formal approach. Indeed, a set of performance metrics have been predicted to show the evolution of the network when the number of nodes increases. |
| Sommaire : |
Contents Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ii Résumé . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iii Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iv General Introduction 1 I WSNs MAC Protocols, Formal Methods and Machine Learning 7 I.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 I.2 Wireless Sensor Network Protocols . . . . . . . . . . . . . . . . . . . . . 8 I.2.1 (Wireless) Sensor Node . . . . . . . . . . . . . . . . . . . . . . 8 I.2.2 Wireless Sensor Networks Definition . . . . . . . . . . . . . . . 9 I.2.3 Main requirements of Wireless Sensor Networks . . . . . . . . . 11 I.2.4 WSNs Medium Access Control Protocols . . . . . . . . . . . . . 12 I.2.5 Energy Harvesting WSNs . . . . . . . . . . . . . . . . . . . . . 17 I.3 Formal Analysing and Verification methods . . . . . . . . . . . . . . . . 18 I.3.1 Hierarchical Timed Coloured Petri Nets . . . . . . . . . . . . . . 19 I.3.2 Linear Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . 25 I.4 Machine Learning for Prediction . . . . . . . . . . . . . . . . . . . . . . 26 I.4.1 Machine Learning Definition . . . . . . . . . . . . . . . . . . . . 27 I.4.2 Machine Learning Algorithms . . . . . . . . . . . . . . . . . . . 27 I.4.3 Machine learning process . . . . . . . . . . . . . . . . . . . . . 29 I.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 II First Contribution: Using Hierarchical Timed Coloured Petri Nets in the Formal Study of CSMA/CA Protocol 33 II.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 II.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 II.3 Modelling CSMA/CA with Hierarchical Timed Coloured Petri Nets . . . 36 II.3.1 The global HTCPN model . . . . . . . . . . . . . . . . . . . . . 38 II.3.2 CPN model for Sensors . . . . . . . . . . . . . . . . . . . . . . . 38 II.3.3 HTCPN model for Base Station . . . . . . . . . . . . . . . . . . 41 II.4 Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 II.4.1 Verification of Qualitative Properties . . . . . . . . . . . . . . . . 45 vCONTENTS CONTENTS II.4.2 Verification of Quantitative Properties . . . . . . . . . . . . . . . 48 II.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 III Second Contribution: Performance Evaluation of CSMA/CA Protocol in Energy Harvesting Wireless Sensor Networks 55 III.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 III.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 III.3 Modelling CSMA/CA using Hierarchical Timed-CPNs . . . . . . . . . . 58 III.3.1 The Global HTCPN Model . . . . . . . . . . . . . . . . . . . . . 58 III.3.2 CPN model for a sensor node . . . . . . . . . . . . . . . . . . . 59 III.3.3 HTCPN model for Base Station . . . . . . . . . . . . . . . . . . 66 III.4 Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 III.4.1 Verification of qualitative properties . . . . . . . . . . . . . . . . 68 III.4.2 Verification of quantitative properties . . . . . . . . . . . . . . . 70 III.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 IV Third Contribution: Using Machine Learning in the Study of Scalability 78 IV.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 IV.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 IV.3 Scalability of the Proposed Approach . . . . . . . . . . . . . . . . . . . 81 IV.3.1 Modelling Phase and Scalability Study . . . . . . . . . . . . . . 82 IV.3.2 Analysis Phase and Scalability Study . . . . . . . . . . . . . . . 82 IV.4 Prediction of Temporal Performance Metrics . . . . . . . . . . . . . . . . 86 IV.4.1 Simulation Results . . . . . . . . . . . . . . . . . . . . . . . . . 86 IV.4.2 Performance Evaluation Prediction . . . . . . . . . . . . . . . . 88 IV.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 General Conclusion 91 v |
| En ligne : | http://thesis.univ-biskra.dz/5508/1/Th%C3%A8se_Zroug_Siham.pdf |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| TINF/164 | Théses de doctorat | bibliothèque sciences exactes | Consultable |
