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...

• Type: Conference
• Year: 2007
• Where: FMOODS
• Authors: Peter Csaba Ölveczky, Stian Thorvaldsen
• Keywords: FMOODS 2007, Formal Methods, Formal Specification, Real-Time Maude, Wireless Sensor Network