A state-based model of sensor protocols

We introduce a state-based model that can be used in specifying and verifying the desired properties of sensor network protocols. This model accommodates several characteristics that are common in sensor networks. Examples of these characteristics are unavoidable local broadcast, probabilistic message transmission, asymmetric communication, message collision, and timeout actions and randomization steps. We also propose three methods for analyzing a sensor network protocol specified in the model. In the first method, called nondeterministic analysis, a specified sensor network protocol is shown to be “nondeterministically correct” under the assumption that message delivery is assured and message collision is guaranteed not to occur. In the second method, called probabilistic analysis, the protocol is shown to be “probabilistically correct” under the assumption that message delivery is probabilistic but message collision is guaranteed not to occur. In the third method, called collision analysis, the effect of message collision and probabilistic message delivery on the correctness of the protocol is analyzed. To demonstrate the utility of our model, we discuss an example protocol that can be used by a sensor to identify its strong neighbors in the network, and apply the analysis methods to the protocol. Using our model, we also show that the protocol satisfies a desirable property, called self-stabilization property.