Formal specification and analysis of performance variation in sensor network diffusion protocols
Sule Nair, Rachel Cardell‐Oliver · 2004
Discovering a routing tree for gathering or disseminating streams of data is an important operation in many sensor network applications. However, protocols for tree discovery may have significant performance problems for certain configurations of a network and its application task.A Temporal Logic of Actions (TLA) specification of push and pull diffusion is introduced in order to analyse such problems. This specification can be used as a basis for implementation, for visualising protocol behaviours, for simulation experiments, and for formal verification of properties of the protocol.This short paper shows how such a specification is used to understand variations in the routing trees discovered by push and pull diffusion and the effect of their shape and size on protocol performance.