Towards the Formal Performance Analysis of Wireless Sensor Networks

The performance of Wireless Sensor Networks (WSNs) is traditionally analyzed using simulation or paper-and-pencil proof methods. However, such methods cannot ascertain accurate analysis, which is a serious drawback for safety and financial-critical applications. In order to overcome this limitation, we propose to use a higher-order-logic theorem prover (HOL) to formally analyze the performance of WSNs. In particular, this paper presents a generic formal performance analysis methodology for WSNs using the k-set randomized scheduling as an energy saving approach. The proposed methodology is primarily based on the formalized theories of measure and probability. For illustration purposes, we formally analyze the performance of a WSN deployed for volcanic earthquake detection.