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

ZROUG, SIHAM (2021) Modelling, verification and performance evaluation of the CSMA/CA protocol in WSNs, by Coloured Petri Nets. Doctoral thesis, Université de mohamed kheider biskra.

[img] Text

Download (39MB)


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.

Item Type: Thesis (Doctoral)
Uncontrolled Keywords: Medium Access Control, Wireless Sensor Networks, CSMA/CA, EHWSNs, Formal Modelling, Formal Analysing, Performance Evaluation, Coloured Petri nets, Linear Temporal Logic. Machine Learning
Subjects: Q Science > Q Science (General)
Divisions: Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie > Département d'informatique
Depositing User: BFSE
Date Deposited: 13 Sep 2021 08:52
Last Modified: 13 Sep 2021 08:52

Actions (login required)

View Item View Item