Login | Register

Formalization of Continuous Time Markov Chains with Applications in Queueing Theory


Formalization of Continuous Time Markov Chains with Applications in Queueing Theory

Chaouch, Donia (2015) Formalization of Continuous Time Markov Chains with Applications in Queueing Theory. Masters thesis, Concordia University.

Text (application/pdf)
Chaouch_MSc_S2015.pdf - Accepted Version
Available under License Spectrum Terms of Access.


The performance analysis of engineering systems have become very critical due to their usage in safety and mission critical domains such as military and biomedical devices. Such an analysis is often carried out based on the Markovian (or Markov Chains based) models of underlying software and hardware components. Furthermore, some important properties can only be captured by queueing theory which involves Markov Chains with continuous time behavior. Classically, the analysis of such models has been performed using paper-and-pencil based proofs and computer simulation, both of which cannot provide perfectly accurate results due to the error-prone nature of manual proofs and the non-exhaustive nature of simulation. Recently, model checking based formal methods have also been used to analyze Markovian and queuing systems. However, such an approach is only applicable for small systems and cannot certify generic properties due to the sate-space explosion problem.
In this thesis, we propose to use higher-order-logic theorem proving as a complementary approach to conduct the formal analysis of queueing systems. To this aim, we present the higher-order-logic formalization of the Poisson process which is the foremost step to model queueing systems. We also verify some of its classical properties such as exponentially distributed inter-arrival time, memoryless property and
independent and stationary increments. Moreover, we used the formalization of the Poisson process to model and verify the error probability of a generic optical communication system. Then we present the formalization of Continuous-Time Markov Chains along with the Birth-Death process. Lastly, we demonstrate the utilization of our developed infrastructure by presenting the formalization of an M/M/1 queue which is widely used to model telecommunication systems. We also formally verified the generic result about the average waiting time for any given queue.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Chaouch, Donia
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:18 March 2015
Thesis Supervisor(s):Tahar, Sofiène
ID Code:979760
Deposited On:13 Jul 2015 13:15
Last Modified:18 Jan 2018 17:49
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