Probabilistic verification of sensor networks
Akim Demaille, Thomas Hérault, Sylvain Peyronnet · 2006
Abstract — Sensor networks are networks consisting of minia-ture 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 changes 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 model a simple sensor network whose aim is to detect an event in a bounded area (such as a fire in a forest). The behavior of the network is probabilistic, so we use Approximate Probabilistic Model Checker (APMC), a tool that allows to approximately check the correctness of extremely large probabilistic systems, to verify it. I.