Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude

摘要

The purpose of this paper is to show how the rewriting-logic-based Real-Time Maude language and tool can be used to formally model, simulate, and model check advanced wireless sensor network (WSN) algorithms. This is done by first proposing some general techniques for modeling and analyzing WSN algorithms, and then by showing how these techniques have been applied to the modeling, performance estimation, and model checking of the state-of-the-art optimal geographical density control (OGDC) density control 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, spatial entities, time-dependent and probabilistic features, and the need to analyze both correctness and performance. We focus on Monte Carlo simulations to evaluate the performance of OGDC. Extensive simulations with up to 800 sensor nodes, and comparison with the ns-2 simulations of OGDC, indicate that Real-Time Maude simulations provide fairly accurate performance estimates of WSN algorithms. As a consequence, simulating the high-level Real-Time Maude model of a WSN algorithm eliminates the need for implementing it on a simulation tool to get a faithful estimate of its performance, while providing much greater flexibility in defining the appropriate simulation scenario; in addition, Real-Time Maude model checking can search for "corner case" bugs and evaluate best-case and worst-case performance. Some of the techniques presented in this paper are also used in an ongoing analysis effort of another state-of-the-art WSN algorithm.