Performance analysis of multi-services call admission control in cellular network using probabilistic model checking

Abstract

This paper deals with formal verification to evaluate performances of Call Admission Control (CAC) schemes in cellular mobile network. Call Admission Control is a mechanism regulating cellular network access to ensure QoS provisioning. From the fact that cellular networks have many classes of services and each class has different QoS requirements, we study CAC schemes supporting two classes of services, real time (RT) and non-real time (NRT), and for each class we distinguish two types of calls, handoff calls (HCs) and new calls (NCs). The studied CAC schemes give priority to RT calls over NRT calls and to HCs over NCs. Traditionally, performance analysis of CAC schemes is performed using analytic and/or simulation models by computing the main steady-state performance measures: new call blocking probability, handoff call dropping probability and mean channels occupation rate. In this work we propose to employ Continuous-time Stochastic Logic (CSL) to specify QoS requirements using transient and steady-state formulas supported by this formalism. Indeed, CSL is a specification language that can be used for Continuous Time Markov Chains (CTMCs) and offers the flexibility to express both transient and steady-state measures including probabilistic path and steady-state formulas. We model the studied CAC schemes with labelled CTMCs then we formalize QoS requirements of each traffic class with CSL. We perform the verification of the considered formulas with PRISM model checker. A performance comparison of the studied CAC schemes is provided based on verification results.