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

Abstract

This master's thesis investigates the suitability of using the real-time formalism and tool Real-Time Maude to formally model and analyze wireless sensor networks.

Real-Time Maude's applicability to wireless sensor networks is explored by formally modeling and analyzing the recently developed wireless sensor network algorithm the optimal geographical density control algorithm (OGDC). Wireless sensor networks are a relatively new network domain and pose challenges to the flexibility of existing modeling formalisms. These challenges are met by Real-Time Maude in this thesis, where new aspects, such as power consumption and broadcasting with limited range, are naturally modeled, while integrating other aspects of the OGDC algorithm, like modeling coverage areas and probabilistic behavior without any problems. Additionally, the Real-Time Maude model results in a precise specification of the OGDC algorithm at a fairly high level of abstraction.

The OGDC algorithm has previously been simulated in the network targeted simulation tool The Network Simulator (ns-2). In this thesis, I show how analogous simulations can be performed using Real-Time Maude. The results of my simulations deviates somewhat from the results of the simulations using ns-2, for which exact reason was not found (as this is not the focus of this thesis).

Furthermore, I show how Real-Time Maude's other formal analysis capabilities complement simulation tools, by subjecting the OGDC algorithm to state exploration analysis which investigates all behaviors in the system from a given initial state, whereas simulations investigates only one behavior. This analysis is performed on a few nodes, because of the large state space. State space exploration is performed for several chosen initial states in search for design errors in the protocol, but no significant errors were found.