Sciweavers

Share
IPPS
2006
IEEE

Formal modeling and analysis of wireless sensor network algorithms in Real-Time Maude

9 years 6 months ago
Formal modeling and analysis of wireless sensor network algorithms in Real-Time Maude
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.
Peter Csaba Ölveczky, Stian Thorvaldsen
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where IPPS
Authors Peter Csaba Ölveczky, Stian Thorvaldsen
Comments (0)
books