PERFORMANCE EVALUATION OF CALL ADMISSION CONTROL SCHEMES IN MULTI-SERVICE CELLULAR NETWORKS USING PRISM MODEL CHECKER

Call Admission Control (CAC) plays a significant role in providing the desired Quality of Service (QoS) in mobile-cellular networks. This paper extends from a previous work in which we proposed a performance evaluation of CAC schemes in mobile cellular networks supporting two classes of services Real-Time (RT) and Non-Real-Time (NRT). The performance of CAC schemes is traditionally evaluated by computing the following steady-state measures: the new call blocking probability, the handoff call dropping probability, and the mean channels occupation rate. We present, in this paper, a detailed comparative evaluation of different CAC schemes proposed in a previous work using formal methods. Furthermore, we propose quantifying more relevant performance measures using the probabilistic model checking. Indeed, we evaluate the performances of the investigated schemes by computing not only the traditional performance measures, but also transient and path-based performance measures. These measures are specified using the branching-time logic Continuous-time Stochastic Logic (CSL). With CSL, we can express QoS requirements over a selective set of paths through the formal model of the considered CAC schema, which is modeled by Continuous-Time Markov chains (CTMCs). We quantify performance measures by checking CSL formulas using the PRISM model checker.