Abstract
Many components of engineering systems exhibit random and uncertain behaviors that are normally distributed. In order to conduct the analysis of such systems within the trusted kernel of a higher-order-logic theorem prover, in this paper, we provide a higher-order-logic formalization of Lebesgue measure and Normal random variables along with the proof of their classical properties. To illustrate the usefulness of our formalization, we present a formal analysis of the probabilistic clock synchronization in wireless sensor networks.
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
References
Ahmed, W., Hasan, O., Tahar, S., Hamdi, M.S.: Towards the formal reliability analysis of oil and gas pipelines. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 30–44. Springer, Heidelberg (2014)
Billingsley, P.: Probability and Measure. Wiley, New York (2012)
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)
Elson, J., Girod, L., Estrin, D.: Fine-grained network time synchronization using reference broadcasts. ACM SIGOPS Oper. Syst. Rev. 36(SI), 147–163 (2002)
Goldberg, R.R.: Methods of Real Analysis. Wiley, New York (1976)
Hasan, O., Abbasi, N., Tahar, S.: Formal probabilistic analysis of stuck-at faults in reconfigurable memory arrays. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 277–291. Springer, Heidelberg (2009)
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)
Hasan, O., Tahar, S.: Using theorem proving to verify expectation and variance for discrete random variables. Autom. Reasoning 41(3–4), 295–323 (2008)
Hasan, O., Tahar, S.: Performance analysis and functional verification of the stop-and-wait protocol in HOL. Autom. Reasoning 42(1), 1–33 (2009)
Hölzl, J.: Analyzing discrete-time Markov chains with countable state space in Isabelle/HOL (2013). http://home.in.tum.de/hoelzl/classifying/
Hölzl, J., Heller, A.: Three chapters of measure theory in Isabelle/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135–151. Springer, Heidelberg (2011)
Liu, L., Hasan, O., Tahar, S.: Formalization of finite-state discrete-time Markov chains in HOL. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 90–104. Springer, Heidelberg (2011)
Liu, L., Hasan, O., Tahar, S.: Formal analysis of memory contention in a multiprocessor system. In: Iyoda, J., de Moura, L. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 195–210. Springer, Heidelberg (2013)
McInnes, A.I.: Model-checking the flooding time synchronization protocol. In: International Conference on Control and Automation, pp. 422–429. IEEE (2009)
Mhamdi, T., Hasan, O., Tahar, S.: On the formalization of the Lebesgue integration theory in HOL. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 387–402. Springer, Heidelberg (2010)
Mhamdi, T., Hasan, O., Tahar, S.: Formalization of entropy measures in HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 233–248. Springer, Heidelberg (2011)
Mhamdi, T., Hasan, O., Tahar, S.: Evaluation of anonymity and confidentiality protocols using theorem proving. Formal Methods Syst. Des. 47(3), 265–286 (2015)
PalChaudhuri, S., Saha, A.K., Johnson, D.B.: Adaptive clock synchronization in sensor networks. In: Information Processing in Sensor Networks, pp. 340–348. ACM (2004)
Isabelle/HOL Probability Distribution Repository (2016). https://isabelle.in.tum.de/dist/library/HOL/HOL-Probability/Distributions.html
Rice, J.A.: Mathematical Statistics and Data Analysis. Duxbury Press, Pacific Grove (1995)
Schuts, M., Zhu, F., Heidarian, F., Vaandrager, F.: Modelling clock synchronization in the Chess gMAC WSN protocol. In: Quantitative Formal Methods: Theory and Applications. EPTCS, vol. 13, pp. 41–54 (2009)
Zhang, F., Bu, L., Wang, L., Zhao, J., Chen, X., Zhang, T., Li, X.: Modeling and evaluation of wireless sensor network protocols by stochastic timed automata. Electron. Notes Theoret. Comput. Sci. 296, 261–277 (2013)
Acknowledgement
This publication was made possible by NPRP grant # [5 - 813 - 1 134] from the Qatar National Research Fund (a member of Qatar Foundation). The statements made herein are solely the responsibility of the author[s].
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Qasim, M., Hasan, O., Elleuch, M., Tahar, S. (2016). Formalization of Normal Random Variables in HOL. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds) Intelligent Computer Mathematics. CICM 2016. Lecture Notes in Computer Science(), vol 9791. Springer, Cham. https://doi.org/10.1007/978-3-319-42547-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-42547-4_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-42546-7
Online ISBN: 978-3-319-42547-4
eBook Packages: Computer ScienceComputer Science (R0)