Sciweavers

Share
FMOODS
2007

Formal Modeling and Analysis of the OGDC Wireless Sensor Network Algorithm in Real-Time Maude

9 years 1 months ago
Formal Modeling and Analysis of the OGDC Wireless Sensor Network Algorithm in Real-Time Maude
This paper describes the application of Real-Time Maude to the formal specification, simulation, and further formal analysis of the sophisticated state-of-the-art OGDC wireless sensor network algorithm. Wireless sensor networks in general, and the OGDC algorithm in particular, pose many challenges to their formal specification and analysis, including novel communication forms, treatment of geographic areas, time-dependent and probabilistic features, and the need to analyze both correctness and performance. Real-Time Maude extends the rewriting logic tool Maude to support formal specification and analysis of objectbased real-time systems. This paper explains how we formally specified OGDC in Real-Time Maude, how we could simulate our specification to perform all the analyses done by the algorithm developers using the network simulation tool ns-2, and how we could perform further formal analyses which are beyond the capabilities of simulation tools. A remarkable result is that our R...
Peter Csaba Ölveczky, Stian Thorvaldsen
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2007
Where FMOODS
Authors Peter Csaba Ölveczky, Stian Thorvaldsen
Comments (0)
books