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:
