Article ID Journal Published Year Pages File Type
515057 ICT Express 2015 4 Pages PDF
Abstract

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.

Related Topics
Physical Sciences and Engineering Computer Science Computer Science Applications
Authors
, , , ,