Design and analysis of self-stabilizing sensor network protocols

A sensor is a battery-operated small computer with an antenna and a sensing board that can sense magnetism, sound, heat, etc. Sensors in a network communicate and cooperate with other sensors to perform given tasks. A sensor network is exposed to various dynamic factors and faults, such as topology changes, energy saving features, unreliable communication, and hardware/software failures. Thus, protocols in this sensor network should be able to adapt to dynamic factors and recover from faults. In this dissertation, we focus on designing and analyzing a class of sensor network protocols, called self-stabilizing protocols. A self-stabilizing protocol is guaranteed to return to a state where it performs its intended function correctly, when some dynamic factors or faults corrupt the state of the protocol arbitrarily. Therefore, in order to make a sensor network resilient to dynamic factors and faults, each protocol in the sensor network should be self-stabilizing. We first develop a state-based model that can be used to formally specify sensor network protocols. This model accommodates several unique characteristics of sensor networks, such as unavoidable local broadcast, probabilistic message transmission, asymmetric communication, message collision, and timeout actions and randomization steps. Second, we present analysis methods for verifying and analyzing the correctness and self-stabilization properties of sensor network protocols specified in this model. Third, using the state-based model and analysis methods, we design three self-stabilizing sensor network protocols, prove their self-stabilization properties, and estimate their performance. These three self-stabilizing protocols are a sentry-sleeper protocol that elects a sentry from a group of sensors at the beginning of each time period, a logical grid routing protocol that builds a routing tree whose root is the base station, and a family of flood sequencing protocols that distinguish between fresh and redundant flood messages using sequence numbers.