Comparative Analysis of Clustering Protocols with Probabilistic Model Checking

Wireless sensor networks with hundreds of sensor nodes have emerged in recent years as important platforms for a wide spectrum of monitoring tasks ranging from environmental to military applications. In order to support scalability and increase lifetime of these networks, sensor nodes are preferably grouped into clusters. A large number of clustering protocols have been proposed in the literature with different aims, requirements and efficiency. Previous comparative studies of such protocols were usually based on simulation, which, however, only provides average case results on the limited state space explored. To mend this situation, in this paper, we evaluate and compare four state-of-the-art clustering protocols, i.e., LEACH, GENLEACH, HEED and PANEL, with full state space exploration. Within our analytical framework that consists of a network configuration and an energy consumption model, we aim at analyzing the correctness and performance of the investigated protocols. Our analysis is conducted formally through probabilistic model checking using PRISM and has its focus on the quantitative aspects of the protocols.