Formal modeling and analysis of wireless sensor network algorithms in Real-Time Maude
Peter Csaba Ölveczky, Stian Thorvaldsen · 2006
Abstract — Advanced wireless sensor network algorithms pose challenges to their formal modeling and analysis, such as model-ing probabilistic and real-time behaviors and novel forms of com-munication, 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 analyze the sophisticated OGDC algorithm. 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. We have modeled the OGDC algorithm in Real-Time Maude at a suitable level of abstraction, and 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. Furthermore, we believe that modeling and simulating the OGDC algorithm in Real-Time Maude require significantly less effort than implementing it on a simulation tool. This paper shows how typical features of wireless sensor networks can be modeled in Real-Time Maude, and briefly summarizes our modeling and analysis of the OGDC algorithm. I.