Formal Probabilistic Analysis of a WSN-Based Monitoring Framework for IoT Applications

Internet of Things (IoT) has been considered as an intuitive evolution of sensing systems using Wireless Sensor Networks (WSN). In this context, energefficiency is considered as one of the most critical requirement. For that purpose, the randomized node scheduling approach is largely applied. The randomness feature in the node scheduling together with the unpredictable deployment make probabilistic techniques much more appropriate to evaluate the coverage properties of WSNs. Classical probabilistic analysis techniques, such as simulation and model checking, do not guarantee accurate results, and thus are not suitable for analyzing mission-critical WSN applications. Based on the most recently developed probability theory, available in the HOL theorem prover, we develop the formalizations of the key coverage performance attributes: the coverage intensity of a specific point and the expected value of the network coverage intensity. The practical interest of our higher-order-logic developments is finally illustrated through formally analyzing the asymptotic coverage behavior of an hybrid monitoring framework for environmental IoT.