Modelling, verification and performance evaluation of the CSMA/CA protocol in WSNs, by Coloured Petri Nets

Abstract

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.