Advanced wireless sensor network algorithms pose challenges to their
formal modeling and analysis, such as modeling
probabilistic and real-time behaviors and novel forms of
communication, and analyzing both correctness and
performance. In this paper, we propose using Real-Time Maude to
formally model, simulate, and further analyze such algorithms. The
Real-Time Maude formalism is expressive yet intuitive, and the tool
provides a spectrum of analysis methods, including simulation,
reachability analysis, and temporal logic model checking.
We have used Real-Time Maude to formally model and
analyze the sophisticated OGDC
algorithm. We
could perform all the analyses performed by
the OGDC developers using the simulation tool ns-2, as well as further
analyses which are beyond the capabilities of simulation
tools. To the best of our knowledge, this is the first time a formal
tool has been applied to such
a complex wireless sensor network algorithm.
Download paper: pdf.