Probabilistic Verification of Sensor Networks
From LRDE
- 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
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.}
}