This master's thesis investigates the suitability of using thereal-time formalism and tool Real-Time Maude to formally model andanalyze wireless sensor networks.
Real-Time Maude's applicability to wireless sensor networks isexplored by formally modeling and analyzing the recently developedwireless sensor network algorithm the optimal geographicaldensity control algorithm (OGDC). Wireless sensor networks are arelatively new network domain and pose challenges to the flexibilityof existing modeling formalisms. These challenges are met by Real-TimeMaude in this thesis, where new aspects, such as power consumption andbroadcasting with limited range, are naturally modeled, whileintegrating other aspects of the OGDC algorithm, like modelingcoverage areas and probabilistic behavior without any problems.Additionally, the Real-Time Maude model results in a precisespecification of the OGDC algorithm at a fairly high level ofabstraction.
The OGDC algorithm has previously been simulated in the networktargeted simulation tool The Network Simulator (ns-2). In thisthesis, I show how analogous simulations can be performed usingReal-Time Maude. The results of my simulations deviates somewhat fromthe results of the simulations using ns-2, for which exact reason wasnot found (as this is not the focus of this thesis).
Furthermore, I show how Real-Time Maude's other formal analysiscapabilities complement simulation tools, by subjecting the OGDCalgorithm to state exploration analysis which investigates allbehaviors in the system from a given initial state, whereassimulations investigates only one behavior. This analysis isperformed on a few nodes, because of the large state space. Statespace exploration is performed for several chosen initial states insearch for design errors in the protocol, but no significant errorswere found.