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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

73 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017)
EditorsHolger Hermanns, Peter H. Höfner
Pages117-128
Number of pages12
DOIs
Publication statusPublished - 15 Mar 2017
Event2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017)

- Uppsala, Sweden
Duration: 29 Apr 201729 Apr 2017
Conference number: 2
http://mars-workshop.org/mars2017/

Workshop

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

Abbreviated titleMARS 2017
CountrySweden
CityUppsala
Period29/04/1729/04/17
Internet address

Fingerprint Dive into the research topics of 'Modelling and verification of a cluster-tree formation protocol implementation for the IEEE 802.15.4 TSCH MAC operation mode.'. Together they form a unique fingerprint.

  • Cite this

    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 (Eds.), Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017) (pp. 117-128) https://doi.org/10.4204/EPTCS.244.5