Login | Register

Formalization of Normal Random Variables

Title:

Formalization of Normal Random Variables

Qasim, Muhammad (2016) Formalization of Normal Random Variables. Masters thesis, Concordia University.

[img]
Preview
Text (application/pdf)
thesis.pdf - Accepted Version
761kB

Abstract

Engineering systems often have components that exhibit random behavior. This randomness in many cases is normally distributed. To verify such systems, proba- bilistic analysis is used. Such engineering systems have applications in domains like transportation, medicine and military. Despite the safety-critical nature of these ap- plications, most of the analysis is done using informal techniques like simulation and paper-and-pencil analysis, and thus cannot be completely relied upon. The unreliable results produced by such methods may result in heavy financial loss or even the loss of a human life. To overcome the limitation of traditional methods, we propose to conduct the analysis of such systems within the trusted kernel of a higher-order-logic theorem prover HOL4. The soundness and the deduction style of the theorem prover guarantee the validity of the analysis and the results of this type of analysis are generic and valid for any instance of the system. For this purpose, we provide HOL4 formalization of Lebesgue measure and normal random variables along with the proof of their classical properties. We also ported the theory of Gauge integral and other required foundational concepts from HOL Light and Isabelle/HOL theorem provers. To illustrate the usefulness of our formalization, we conducted the formal analysis of two applications, i.e., error probability of binary transmission in the presence of Gaussian noise and probabilistic clock synchronization in wireless sensor networks.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Qasim, Muhammad
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:15 April 2016
Thesis Supervisor(s):Tahar, Sofiène
Keywords:Normal Random Variables, Theorem Proving, HOL4
ID Code:981091
Deposited By: MUHAMMAD QASIM
Deposited On:15 Jun 2016 16:11
Last Modified:18 Jan 2018 17:52
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Back to top Back to top