Real-Time Maude Case Study: The OGDC Algorithm for Wireless Sensor Networks

The field of wireless sensor networks requires new and sophisticated algorithms/protocols because of, e.g., the focus on energy conservation. The analysis of such networks pose a set of challenges to formal methods and tools, for reasons which may include: (i) the power consumption is usually a critical metric that must be taken into account, (ii) communication is "limited-range" broadcast (which may be subjected to transmission delays) when done by radio, (iii) the topology is often not known in advance and is ever-changing due to nodes dying or becoming inactive, (iv) timers are often needed, (v) for this coverage algorithm, one must also model geometric areas, and related problems (is an area covered by the sensing areas of set of nodes? is the whole sensing area covered by the active nodes?), (vi) the number of nodes is often very large, and (vii) "random" or probabilistic behaviors.

We conjecture that Real-Time Maude, with its expressive and flexible formalism, is an interesting candidate for high-level formal modeling and analysis of advanced wireless sensor network algorithms. Jennifer Hou at the University of Illinois at Urbana-Champaign suggested to us to model her and Zhang's recently developed OGDC wireless sensor network algorithm as a challenge for formal tools. The OGDC algorithm aims at maintaining complete sensing coverage of a certain area for as long as possible. By complete coverage we mean that, for any point in the area, there is an active node whose own sensing area covers this point. That is, no matter where something to be observed happens, there is an active sensor node which can observe the event. To maintain complete coverage for as long as possible, nodes are turned off and on according to sophisticated computations. The authors claim that ns-2 simulations show that OGDC outperforms existing density control algorithms with respect to network lifetime.

Stian Thorvaldsen at the University of Oslo, in joint work with Peter Ölveczky, has modeled and analyzed the OGDC algorithm in Real-Time Maude. His master's thesis describes this effort. We have since, in joint work, modified the specification somewhat.

We have modeled the protocol in Real-Time Maude (in the process addressing all the challenges listed above), and have performed some analysis. We have done all the simulations corresponding to the ns-2 simulations performed by the algorithm developers. In addition, we have done some state space exploration analysis.

The interesting results of our analysis are the following:

  1. We have simulated OGDC (with 5 different initial seed values for the random function which, among other things, is used to generate the "random" locations of the node) for 200, 400, and 600 sensor nodes in the sensing area, with all the parameter values as suggested in Zhang & Hou's journal paper on OGDC (see below). Our simulations show a significantly higher number of nodes set to "active" than in the ns-2 simulations. Since transmission delays play a significant role in the definition of OGDC, we have included such delays in our model.
  2. When we ignore transmission delays in our Real-Time Maude simulations, the OGDC performance figures are in fairly close correspondence with the performance figures obtained in the ns-2 simulations.
  3. We have heard from Professor Hou that it is quite likely that their ns-2 simulations did not take transmission delays into account. Repeated email requests to the person responsible for the actual ns-2 have unfortunately not been answered.
  4. We can point to a "flaw" in the definition of the OGDC algorithm that explains the much worse performance in the presence of transmission delays.
  5. It is therefore tempting to conclude that Real-Time Maude simulations provide more accurate performance estimates than the ns-2 simulations.
  6. We have model checked some correctness properties for systems up to 6 nodes without finding any flaws.

March 15, 2007: Conference paper (extended with an appendix) that describes specification and our simulation results for both the delayed and delay-less setting is now available.

Related Papers

  1. Formal Modeling and Analysis of the OGDC Wireless Sensor Network Algorithm in Real-Time Maude.
    By Peter C. Ölveczky and Stian Thorvaldsen.
    To appear in FMOODS 2007.
    This is a paper that explains the specification of OGDC and the simulation results in the different settings, as well as giving some model checking commands. More recent than the references below.
  2. Formal Modeling and Analysis of the OGDC Wireless Sensor Network Algorithm in Real-Time Maude.
    By Stian Thorvaldsen and Peter C. Ölveczky.
    26 page report on our work. This is the main reference to our work on the OGDC algorithm. Also available in ps format.
    (This version adds an appendix containing the whole Real-Time Maude specification (in ps format)).
  3. Formal Modeling and Analysis of Wireless Sensor Network Algorithms in Real-Time Maude.
    By Peter C. Ölveczky and Stian Thorvaldsen.
    This paper is a quite short (8 pages) paper invited to a session on real-time issues in wireless sensor networks at the The 14th International Workshop on Parallel and Distributed Real-Time Systems 2006, held in conjunction with IPDPS 2006.
    The paper is more a "high-level" paper that motivates why Real-Time Maude may be suitable to specify and analyze wireless sensor networks. It presents a brief overview of some general techniques for modeling wireless sensor network algorithms in Real-Time Maude and only very briefly summarizes the OGDC case study. (A paper that deals more explicitly with OGDC has been submitted to a conference.)
  4. Modeling and Analysis of the OGDC Wireless Sensor Network Algorithm in Real-Time Maude.
    By Stian Thorvaldsen.
    Master's Thesis, Department of Informatics, University of Oslo, June 2005.
    This is an extensive report on the Real-Time Maude 2.1 specification and analysis of the OGDC algorithm. Essentially superseded by the report (2) above.
  5. Maintaining Sensing Coverage and Connectivity in Large Sensor Networks.
    By Honghai Zhang and Jennifer C. Hou.
    Ad Hoc & Sensor Wireless Networks, Volume 1, Number 1-2, 2005
    Gives an overview of the OGDC algorithm

The Executable Real-Time Maude 2.2 Specification of OGDC

Update: The Executable Real-Time Maude 2.3 Specifications of OGDC
We have very slightly modified our specifications (a RTM 2.2 spec also executes on RTM 2.3), and have defined a version that uses Maude's built-in Mersenne Twister pseudo-random number generator instead of our home-made one. The difference in performance estimates is not significant.

Many more results will be added next week if I don't forget!


Peter Ölveczky