Formal Probabilistic Analysis of a Wireless Sensor Network for Forest Fire Detection
Adel Bouhoula, Tetsuo Ida, Fairouz Kamareddine (eds, M. Elleuch, Osman Hasan, Mohamed Nadhir Abid · 2012
Wireless Sensor Networks (WSNs) have been widely explored for forest fire detection, which is con-sidered 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 per-formance 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 us-ing 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. 1