Probabilistic Verification of Sensor Networks

Authors

Akim Demaille, Sylvain Peyronnet, Thomas Hérault

Where

Proceedings of the Fourth International Conference on Computer Sciences, Research, Innovation and Vision for the Future (RIVF'06)

Place

Ho Chi Minh City, Vietnam

Type

inproceedings

Projects

APMC

Date

2006-02-01

Abstract

Sensor networks are networks consisting of miniature and low-cost systems with limited computation power and energy. Thanks to the low cost of the devices, one can spread a huge number of sensors into a given area to monitor, for example, physical change of the environment. Typical applications are in defense, environment, and design of ad-hoc networks areas. In this paper, we address the problem of verifying the correctness of such networks through a case study. We modelize a simple sensor network whose aim is to detect the apparition of an event in a bounded area (such as a fire in a forest). The behaviour of the network is probabilistic, so we use APMC, a tool that allows to approximately check the correctness of extremely large probabilistic systems, to verify it.

Documents

• Paper

• Slides

Bibtex (lrde.bib)

@InProceedings{	  demaille.06.rivf,
  author	= {Akim Demaille and Sylvain Peyronnet and Thomas H\'erault},
  title		= {Probabilistic Verification of Sensor Networks},
  booktitle	= {Proceedings of the Fourth International Conference on
		  Computer Sciences, Research, Innovation and Vision for the
		  Future (RIVF'06)},
  year		= 2006,
  address	= {Ho Chi Minh City, Vietnam},
  isbn		= {1-4244-0316-2},
  month		= feb,
  abstract	= {Sensor networks are networks consisting of miniature and
		  low-cost systems with limited computation power and energy.
		  Thanks to the low cost of the devices, one can spread a
		  huge number of sensors into a given area to monitor, for
		  example, physical change of the environment. Typical
		  applications are in defense, environment, and design of
		  ad-hoc networks areas. In this paper, we address the
		  problem of verifying the correctness of such networks
		  through a case study. We modelize a simple sensor network
		  whose aim is to detect the apparition of an event in a
		  bounded area (such as a fire in a forest). The behaviour of
		  the network is probabilistic, so we use APMC, a tool that
		  allows to approximately check the correctness of extremely
		  large probabilistic systems, to verify it.}
}