Performance Analysis of ARQ Protocols using a Theorem Prover

Automatic-repeat-request (ARQ) protocols are widely used in modern data communications to guarantee reliable transmission over imperfect physical links. The behavior of an ARQ protocol largely depends on a number of network parameters and traditionally simulation is used for their performance analysis. However, simulation provides less accurate results and usually requires enormous amount of CPU time in order to attain reasonable estimates. To overcome these limitations, we propose to conduct the performance analysis of ARQ protocols in the environment of a higher-order-logic theorem prover (HOL). We present an approach to formally model the delay characteristics of ARQ protocols as a function of geometric random variable in higher-order-logic. In particular, we develop higher-order-logic models that describe the delay behavior of three basic types of ARQ protocols, i.e., Stop-and-Wait, Go-Back-N and Selective-Repeat. The paper also includes the verification of the average message delay relations for these three protocols in HOL.