Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Aslan, Y., Korpeoglu, I., Ulusoy, O.: A framework for use of wireless sensor networks in forest fire detection and monitoring. Comput. Environ. Urban Syst. 36(6), 614–625 (2012)
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Ballarini, P., Miller, A.: Model checking medium access control for sensor networks. In: Proceedings of the 2nd Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 255–262. IEEE Computer Society (2006)
Bernardeschi, C., Masci, P., Pfeifer, H.: Analysis of wireless sensor network protocols in dynamic scenarios. In: Guerraoui, R., Petit, F. (eds.) SSS 2009. LNCS, vol. 5873, pp. 105–119. Springer, Heidelberg (2009). doi:10.1007/978-3-642-05118-0_8
Elleuch, M.: Formalization of the coverage properties of WSNs in HOL (2015). http://hvg.ece.concordia.ca/projects/prob-it/wsn.php
Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal analysis of a scheduling algorithm for wireless sensor networks. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 388–403. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24559-6_27
Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal probabilistic analysis of a wireless sensor network for forest fire detection. In: Symbolic Computation in Software Science, Electronic Proceedings in Theoretical Computer Science, vol. 122, pp. 1–9. Open Publishing Association (2013)
Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Towards the formal performance analysis of wireless sensor networks. In: Proceedings of the 22nd Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, pp. 365–370. IEEE Computer Society (2013)
Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal probabilistic analysis of detection properties in wireless sensor networks. Formal Aspects Comput. 27(1), 79–102 (2015)
Fehnker, A., Fruth, M., McIver, A.K.: Graphical modelling for simulation and formal analysis of wireless network protocols. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Methods, Models and Tools for Fault Tolerance. LNCS, vol. 5454, pp. 1–24. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00867-2_1
Fruth, M.: Probabilistic model checking of contention resolution in the IEEE 802.15.4 low-rate wireless personal area network protocol. In: Proceedings of the 2nd Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 290–297. IEEE Computer Society (2006)
Hart, J., Martinez, K.: Towards an environmental Internet of Things [IoT]. Earth Space Sci. 2, 1–7 (2015)
Hasan, O.: Formal probabilistic analysis using theorem proving. Ph.D. thesis, Concordia University, Montreal, QC, Canada (2008)
Hasan, O., Tahar, S.: Formalization of continuous probability distributions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 3–18. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73595-3_2
Hölzl, J., Heller, A.: Three chapters of measure theory in Isabelle/HOL. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135–151. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22863-6_12
Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge, Cambridge, UK (2002)
Lazarescu, M.: Design of a WSN platform for long-term environmental monitoring for IoT applications. IEEE J. Emerg. Sel. Topics Circ. Syst. 3(1), 1–6 (2013)
Liu, C., Wu, K., Xiao, Y., Sun, B.: Random coverage with guaranteed connectivity: joint scheduling for wireless sensor networks. IEEE Trans. Parallel Distrib. Syst. 17(6), 562–575 (2006)
MacKay, D.: Introduction to Monte Carlo methods. In: Proceedings of NATO Advanced Study Institute on Learning in Graphical Models, pp. 175–204. Kluwer Academic Publishers (1998)
Mainetti, L., Patrono, L., Vilei, A.: Evolution of wireless sensor networks towards the internet of things: a survey. In: Proceedings of the 19th International Conference on Software, Telecommunications and Computer Networks, pp. 1–6. IEEE (2011)
Mhamdi, T.: Information-theoretic analysis using theorem proving. Ph.D. thesis, Concordia University, Montreal, QC, Canada, December 2012
Ölveczky, P.C., Thorvaldsen, S.: Formal modeling and analysis of the OGDC wireless sensor network algorithm in real-time Maude. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 122–140. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72952-5_8
Rutten, J., Kwaiatkowska, M., Normal, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems. CRM Monograph Series. American Mathematical Society, Providence (2004)
Whitmore, A., Agarwal, A., Xu, L.: The internet of things-a survey of topics and trends. Inf. Syst. Front. 17(2), 261–274 (2015)
Wu, K., Gao, Y., Li, F., Xiao, Y.: Lightweight deployment-aware scheduling for wireless sensor networks. Mob. Netw. Appl. 10(6), 837–852 (2005)
Xiao, Y., Chen, H., Wu, K., Sun, B., Zhang, Y., Sun, X., Liu, C.: Coverage and detection of a randomized scheduling algorithm in wireless sensor networks. IEEE Trans. Comput. 59(4), 507–521 (2010)
Xiao, Y., Zhang, Y.: Divide-and conquer-based surveillance framework using robots, sensor nodes, and RFID tags. Wirel. Commun. Mob. Comput. 11(7), 964–979 (2011)
Yick, J., Mukherjee, B., Ghosal, D.: Wireless sensor network survey. Comput. Netw. 52(12), 2292–2330 (2008)
Zayani, H., Barkaoui, K., Ayed, R.B.: Probabilistic verification and evaluation of backoff procedure of the WSN ECo-MAC protocol. Int. J. Wirel. Mob. Netw. 12(1), 156–170 (2010)
Zheng, M., Sun, J., Liu, Y., Dong, J.S., Gu, Y.: Towards a model checker for NesC and wireless sensor networks. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 372–387. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24559-6_26
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Elleuch, M., Hasan, O., Tahar, S., Abid, M. (2017). Formal Probabilistic Analysis of a WSN-Based Monitoring Framework for IoT Applications. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2016. Communications in Computer and Information Science, vol 694. Springer, Cham. https://doi.org/10.1007/978-3-319-53946-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-53946-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-53945-4
Online ISBN: 978-3-319-53946-1
eBook Packages: Computer ScienceComputer Science (R0)