The performance analysis of engineering systems has become very critical due to their extensive usage in safety and mission critical domains, such as military and biomedical devices. Such an analysis is often carried out based on Queueing theory which involves random processes with continuous time behavior. In this paper, we propose to use higher-order-logic (HOL) theorem proving as a complementary approach to simulation and computer algebra systems to conduct the formal analysis of Queueing systems. As a first step towards this aim, we present the HOL formalization of M/M/1 queue, which is one of the most foundational and widely used model in Queueing theory. The proposed formalization is primarily based on the Poisson process Continuous-Time Markov Chains and the Birth-Death process and thus the paper also presents their formalizations in HOL. To demonstrate the practical utilization of our formalization, we formally analyze a simplistic model of an optical communication system and a queue of an airport runway model.

HOL Script

• Download