Probabilistic Verification of Sensor Networks

From LRDE

Revision as of 11:14, 26 April 2016 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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

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.}
}