Modelling and verification of a cluster-tree formation protocol implementation for the IEEE 802.15.4 TSCH MAC operation mode.

M. Talebi, J.F. Groote, C. Dandelski

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

73 Downloads (Pure)

Samenvatting

Correct and efficient initialization of wireless sensor networks can be challenging in the face of many uncertainties present in ad hoc wireless networks. In this paper we examine an implementation for the formation of a cluster-tree topology in a network which operates on top of the TSCH MAC operation mode of the IEEE 802.15.4 standard, and investigate it using formal methods. We show how both the mCRL2 language and toolset help us in identifying scenarios where the implementation does not form a proper topology. More importantly, our analysis leads to the conclusion that the cluster-tree formation algorithm has a super linear time complexity. So, it does not scale to large networks.
Originele taal-2Engels
TitelProceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017)
RedacteurenHolger Hermanns, Peter H. Höfner
Pagina's117-128
Aantal pagina's12
DOI's
StatusGepubliceerd - 15 mrt 2017
Evenement2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017)

- Uppsala, Zweden
Duur: 29 apr 201729 apr 2017
Congresnummer: 2
http://mars-workshop.org/mars2017/

Workshop

Workshop2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017)

Verkorte titelMARS 2017
LandZweden
StadUppsala
Periode29/04/1729/04/17
Internet adres

Vingerafdruk Duik in de onderzoeksthema's van 'Modelling and verification of a cluster-tree formation protocol implementation for the IEEE 802.15.4 TSCH MAC operation mode.'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Talebi, M., Groote, J. F., & Dandelski, C. (2017). Modelling and verification of a cluster-tree formation protocol implementation for the IEEE 802.15.4 TSCH MAC operation mode. In H. Hermanns, & P. H. Höfner (editors), Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017) (blz. 117-128) https://doi.org/10.4204/EPTCS.244.5