ICT Express (Jun 2015)

Formal Modeling of Greedy Nodes in 802.15.4 WSN

  • Youcef Hammal,
  • Jalel Ben-Othman,
  • Lynda Mokdad,
  • Abdelkrim Abdelli

DOI
https://doi.org/10.1016/S2405-9595(15)30014-X
Journal volume & issue
Vol. 1, no. 1
pp. 10 – 13

Abstract

Read online

This paper deals with formal specification of the non-slotted CSMA/CA protocol in wireless sensor networks(WSN) whose some nodes own a greedy behavior. This protocol requires sensor nodes to wait some time before initiating a transmission, whereas greedy nodes may try to reduce their waiting duration, which may penalize other nodes. To analyze their impact on WSN mode in operation, we use timed automata of the model-checker UPPAAL to capture the abstract behavior of communication medium, sane, and greedy nodes in WSN. This enables the use of analysis tools to check whether these models satisfy intended properties.