Formal Models for the Analysis of Wireless Sensor Network Protocols
Overview
The behaviour of
large-scale wireless sensor networks has been shown to be surprisingly complex
and difficult to analyse, both by empirical experiment, and in simulation. We
are developing new formal models for the behaviour of wireless sensor networks
which model the physical interaction of sensor nodes and their landscape, and
the behaviour of individual nodes following a protocol. A formal model is a precise and
unambiguous, but necessarily abstract, description of a network's behaviour; it
is well suited for describing sensor network properties and for the simulation
and verification of network behaviours.
We have used this model to prove that flooding is unreliable in
multi-hop networks, and to characterise network conditions that lead to
failure. We have also simulated the behaviour of flooding protocols in a sensor
network under different assumptions about the transmission power used by nodes,
the shape of transmission footprint (derived from empirical data), the position
of the nodes within their landscape, and the probability with which a node
chooses to retransmit the flood message. Our wireless sensor network model has
been demonstrated to be a convenient tool for isolating and studying individual
properties of these networks, and thus a useful step towards understanding
their complex behaviour.
The
figure shows a flooding protocol in progress in a 1024 node hexagonal grid
network. Sensor nodes are the grid
of large dots: black (completed), red (trying to send) and green (waiting for
the flood). The small yellow and
blue cells show radio signal: blue for data signals and yellow for noise or interference
signals.
Papers
Formal Specification and
Analysis of Performance Variation in Sensor Network Diffusion Protocols,
Sule Nair and Rachel Cardell-Oliver, In 7th
ACM Symposium on Modeling, Analysis and Simulation of Wireless and Mobile
Systems, Venice, October 2004. a
longer version is available here
Why
Flooding is Unreliable in Multi-hop, Wireless Networks, Rachel
Cardell-Oliver, February 2004, Submitted for Review. Extended version available as Technical Report UWA-CSSE-04-001 February 2004
Evaluating
the Impact of Limited Resource on the Performance of Flooding in Wireless
Sensor Networks, Patrick Downey and
Rachel Cardell-Oliver, December 2003, To appear in the International Conference
on Dependable Systems and Networks, Florence July 2004.
The Behaviour of
A Flooding Protocol In a Wireless Sensor Network, Patrick Downey, Honours Thesis, School of Computer Science &
Software Engineering, The University of Western Australia, December 2003
Web Pages, Software and More Results
Analysis of Diffusion in Sensor Networks,
Sule Nair, July 2004, http://www.csse.uwa.edu.au/~sule/diffusion/
Our analysis of mote transmission footprints
based on the experimental data at http://www.cs.berkeley.edu/~awoo/connectivity/ and
A picture comparing
observed and idealised footprints for different transmission power settings
Patrick Downey, Boris: An Extensible Java Simulator for Wireless Sensor
Networks, January 2004
People
Rachel Cardell-Oliver
Sule Nair (PhD student 2004)
Samantha Chen (Honours 2003-4)
Patrick Downey (Honours 2004)
Page updated 2 July 2004
Paper requests, questions, comments, please email rachel@csse.uwa.edu.au
Rachel
Cardell-Oliver
School of Computer Science & Software Engineering
The University
of Western Australia