Formal Probabilistic Analysis of Wireless Sensor Networks
In the context of Wireless Sensor Networks (WSNs), the randomized scheduling of nodes is
a very common approach to preserve energy.
The main idea of such approach is to
randomly organize the nodes into alternatively working sub-networks. Hence,
during a given time slot, only the nodes belonging to the current active
sub-network are powered up and may report an occurring event while all the other
nodes are inactive and thus contribute to the power saving of the overall system.
Traditionally, paper-and-pencil proof based probabilistic techniques have been
used to analyze the performance of randomized scheduling for WSNs.
Due to the inherent incompleteness of simulation coupled with the
rounding errors of computer arithmetics, such methods cannot be considered as accurate,
which is a serious limitation for mission-critical WSNs.
Formal methods have also been explored for analyzing WSNs but most of the existing work
is focused on analyzing their functional aspects only. However, given the wide application
of WSNs in safety and mission-critical domains, there is a dire need
to accurately assess their performance as well.
In order to overcome the above mentioned limitations, this work provides a formal approach for an accurate analysis of the probabilistic performance properties of WSNs using the k-set randomized scheduling. The above figure depicts the basic building blocks of the proposed methodology while the formalization requirements are represented by the dark grey shaded boxes. The proposed formal performance analysis methodology starts with the formalization of the k-set randomized scheduling algorithm within the HOL theorem prover. After that, the higher-order-logic formalizations of the key performance attributes of the formally specified algorithm, are developed. These performance attributes are the network coverage, the detection and the lifetime. For each of the mentioned performance attribute, a detailed formal asymptotic analysis is developed within the HOL theorem prover as well. Finally, the practical effectiveness of the proposed methodology is shown for analyzing the performance of various real-world applications, such as, environmental outdoor monitoring or enemy intrusion detection.
Publications:
[1] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Formal Probabilistic Analysis of Detection Properties in Wireless Sensor Networks; Formal Aspects of Computing (IF=0.609), Vol. 27, No. 1, pages 79-102. Springer, January 2015,
[2] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Towards the Formal Performance Analysis of Wireless Sensor Networks; 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE'13), Hammamet, Tunisia, June 2013. [Proc. IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, pages 365-370. IEEE Computer Society, 2013.]
[3] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Formal Probabilistic Analysis of a Wireless Sensor Network for Forest Fire Detection; International Symposium on Symbolic Computation in Software Science (SSCS'12), Gammarth, Tunisia, December 2012. [Proc. Symbolic Computation in Software Science, Electronic Proceedings in Theoretical Computer Science (EPTCS 122), pages 1-9. Open Publishing Association, 2013.]
[4] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks; International Conference on Formal Engineering Methods (ICFEM'11), Durham, United Kingdom, October 2011. [In Formal Methods and Software Engineering, LNCS 6991, pages 388-403. Springer-Verlag, 2011.]
[5] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks; Technical Report, Department of Electrical and Computer Engineering, Concordia University, February, 2011. [27 Pages,Old probabilistic framework].
HOL Code:
In order to overcome the above mentioned limitations, this work provides a formal approach for an accurate analysis of the probabilistic performance properties of WSNs using the k-set randomized scheduling. The above figure depicts the basic building blocks of the proposed methodology while the formalization requirements are represented by the dark grey shaded boxes. The proposed formal performance analysis methodology starts with the formalization of the k-set randomized scheduling algorithm within the HOL theorem prover. After that, the higher-order-logic formalizations of the key performance attributes of the formally specified algorithm, are developed. These performance attributes are the network coverage, the detection and the lifetime. For each of the mentioned performance attribute, a detailed formal asymptotic analysis is developed within the HOL theorem prover as well. Finally, the practical effectiveness of the proposed methodology is shown for analyzing the performance of various real-world applications, such as, environmental outdoor monitoring or enemy intrusion detection.
Publications:
[1] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Formal Probabilistic Analysis of Detection Properties in Wireless Sensor Networks; Formal Aspects of Computing (IF=0.609), Vol. 27, No. 1, pages 79-102. Springer, January 2015,
[2] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Towards the Formal Performance Analysis of Wireless Sensor Networks; 22th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE'13), Hammamet, Tunisia, June 2013. [Proc. IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, pages 365-370. IEEE Computer Society, 2013.]
[3] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Formal Probabilistic Analysis of a Wireless Sensor Network for Forest Fire Detection; International Symposium on Symbolic Computation in Software Science (SSCS'12), Gammarth, Tunisia, December 2012. [Proc. Symbolic Computation in Software Science, Electronic Proceedings in Theoretical Computer Science (EPTCS 122), pages 1-9. Open Publishing Association, 2013.]
[4] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks; International Conference on Formal Engineering Methods (ICFEM'11), Durham, United Kingdom, October 2011. [In Formal Methods and Software Engineering, LNCS 6991, pages 388-403. Springer-Verlag, 2011.]
[5] M. Elleuch, O. Hasan, S. Tahar, and M. Abid: Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks; Technical Report, Department of Electrical and Computer Engineering, Concordia University, February, 2011. [27 Pages,Old probabilistic framework].
HOL Code:
- Set_usefulScript.sml (This file contains a set of useful theorems)
- Rand_SchScript.sml (This file contains the foundational formalizations of the randomized scheduling)
- CoverageScript.sml (This file contains the formalization of the network coverage intensity)
- Asymptotic_CoverageScript.sml (This file contains the formalization of the asymptotic network coverage intensity)
- Detection_ProbaScript.sml (This file contains the formalization of the detection probability)
- Asymptotic_ProbaScript.sml (This file contains the formalization of the asymptotic detection probability)
- Detection_DelayScript.sml (This file contains the formalization of the detection delay)
- Asymptotic_DelayScript.sml (This file contains the formalization of the asymptotic detection delay)
