Abstract

Probabilistic techniques play a major role in the design and analysis of wirelesssystems as they contain a significant amount of random or unpredictable components. Traditionally, computer simulation techniques are used to perform probabilisticanalysis of wirelesssystems but they provide inaccurate results and usually require enormous amount of CPU time in order to attain reasonable estimates. To overcome these limitations, we propose to use a higher-order-logic theorem prover (HOL) for the analysis of wirelesssystems. The paper presents a concise description of the formal foundations required to conduct the analysis of a wirelesssystem in a theorem prover, such as the higher-order-logic modeling of random variables and the verification of their corresponding probabilistic and statistical properties in a theorem prover. In order to illustrate the utilization and effectiveness of the proposed idea for handling real-world wirelesssystemanalysis problems, we present an analysis of the automated repeat request (ARQ) mechanism at the logic link control (LLC) layer of the General Packet Radio Service (GPRS), which is a packet oriented mobile data service available to the users of Global System for Mobile Communications (GSM).