Very often the randomness in engineering systems is normally distributed. In this project we formalized normal distribution in higher-order logic. For this purpose, we first provide the formalization of Lebesgue measure based on Henstock-Kurzweil integral and probability density function as Radon Nikodym derivative of probability measure with respect to Lebesgue measure. Then we use probability density function to formalize normal random variables and prove some of their classical properties. We used our formalization to model and verify the probability of error in the transmission of binary signals in the presence of Gaussian noise. We also used it to analyze the probabilistic bounds on the accuracy of clock synchronization technique in wireless sensor network.

HOL Script

• HOL4 source
  
  

Publications

1. M. Qasim, O. Hasan, M. Elleuch and S. Tahar: Formalization of Normal Random Variables in HOL In: M. Kohlhase el at. (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science [Proc. Conference of Intelligent Computer Mathematics (CICM'2016)], To Appear
   
   

Master Thesis

Muhammad Qasim, "Formalization of Normal Random Variables", M.A.Sc., Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, April 2016.