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