|
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:
- 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.
- 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.
- 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.
- 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.
- It is therefore tempting to conclude that Real-Time
Maude simulations provide more accurate performance estimates
than the ns-2 simulations.
- 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.
- 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.
- 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)).
- 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.)
- 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.
-
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
|
- The Real-Time Maude file: ogdc.rtmaude
- How to execute/analyze these specifications?
- Start Real-Time Maude 2.2.
- Load the above file ogdc.rtmaude.
The various analysis commands are given at the end of
this file, but are commented away; just remove the '---'
parts around the commands, or cut-and-paste the desired command onto the Maude
command line.
Please note that many of the rewriting and analysis commands take
some time, even hours, to execute. In a first execution, you may
well want to decrease the number of nodes, or the number of rounds,
significantly.
Also note that the states are quite large, so may want to re-direct
your output to a file, or pipe it to some other program.
- Output from the execution of different commands
with transmission delays:
- Simulate one round with 200 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 400 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 600 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
-
Simulate 50 rounds with 200 nodes
- find latest command with 6 nodes
- model checking stability of steady-state-ness
- search for lack of coverage 1
- search for lack of coverage 2.
- Output from the execution of different commands
without transmission delays:
- Simulate one round with 200 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 400 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 600 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
|
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.
- The executable Real-Time Maude specifications (including
the execution commands): with
old random seed,
with Maude's built-in random random
number generator,
with
old random seed and no delay, and
with
Maude's built-in random random
number generator and no transmission delay
- Output from execution with old random number generator and
with transmission delays:
- Simulate one round with 200 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 400 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 600 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 800 nodes:
initial seed 1.
- Simulate 50 rounds with 300 nodes:
initial seed 1.
- Simulate 50 rounds with 75 nodes:
initial seed 1.
- Find earliest and latest time steady state phase is reached (5 nodes):
initial seed 97,
initial seed 1,
initial
seed 313,
initial
seed 341.
- Output from execution with old random number generator and
without transmission delays:
- Simulate one round with 200 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 400 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 600 nodes:
initial seed 1,
initial seed 5,
initial seed 97,
initial seed 313, and
initial seed 341.
- Simulate one round with 800 nodes:
initial seed 1.
- Simulate 90 rounds with 300 nodes:
initial seed 1.
Peter
Ölveczky