Formal Probabilistic Analysis of a Wireless Sensor Network for Forest Fire Detection

TL;DR

This paper applies formal probabilistic theorem proving to accurately analyze the performance of a wireless sensor network designed for forest fire detection, focusing on energy efficiency and coverage guarantees.

Contribution

It introduces a formal probabilistic analysis method using theorem proving for WSNs, improving accuracy over traditional simulation and proof techniques.

Findings

Verified expected coverage intensity

Established upper bounds on disjoint subsets

Determined lower bounds on total sensor nodes

Abstract

Wireless Sensor Networks (WSNs) have been widely explored for forest fire detection, which is considered a fatal threat throughout the world. Energy conservation of sensor nodes is one of the biggest challenges in this context and random scheduling is frequently applied to overcome that. The performance analysis of these random scheduling approaches is traditionally done by paper-and-pencil proof methods or simulation. These traditional techniques cannot ascertain 100% accuracy, and thus are not suitable for analyzing a safety-critical application like forest fire detection using WSNs. In this paper, we propose to overcome this limitation by applying formal probabilistic analysis using theorem proving to verify scheduling performance of a real-world WSN for forest fire detection using a k-set randomized algorithm as an energy saving mechanism. In particular, we formally verify the expected values of coverage intensity, the upper bound on the total number of disjoint subsets, for a given coverage intensity, and the lower bound on the total number of nodes.