Formal analysis of a bio-inspired wireless sensor network routing algorithm

Abstract

Wireless Sensor Networks (WSN) are becoming more common and applied in many areas like healthcare, environment monitoring and security. Also, it is increasing the complexity and the network interoperability as heterogeneous sensor nodes are used to compose WSN for emerging applications. Observing the importance of guaranteeing certain properties in the operation of this networks, this paper presents a formal study of a bio-inspired WSN routing algorithm using a probabilistic model to verify properties of this routing algorithm. It is noteworthy to mention the dynamic behavior of the WSN under concern, which is composed of static and mobile nodes, these last ones represented by Unmanned Aerial Vehicles (UAV). This fact adds complexity to the proposed analysis, but presents opportunities for interesting investigations. The acquired results shows that the algorithm is deadlock and livelock free, besides the evaluation of other properties that are also formally verified.