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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Ahmed, M.H.: Call admission control in wireless networks: a comprehensive survey. In: IEEE Communications Surveys and Tutorials, pp. 49–68 (2005)
Alagu, S., Meyyappan, T.: An efficient call admission control scheme for handling handoffs in wireless mobile networks. IJANS 2(3) (2012)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking continuous time Markov chains. ACM Trans. Comput. Log. 1(1), 162–170 (2000)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358–372. Springer, Heidelberg (2000). doi:10.1007/10722167_28
Belghith, A., Mohamed, M.B., Obaidat, M.S.: Efficient bandwidth call admission control in 3Gpp. LTE networks. In: GLOBECOM (2016)
Bisdikian, C., Choi, Y., Kwon, T., Naghshineh, M.: Call admission control for adaptive multimedia in wireless/mobile networks. In: Proceedings of the IEEE Wireless Communications and Networking Conference, vol. 2, pp. 540–544 (1999)
Clarke, E.M., Emerson, A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)
Cornefjord, M., Gaasvik, P.-O., Svensson, V.: Different methods of giving priority to handoff traffic in a mobile telephone system with directed retry. In: Proceedings of the 41st IEEE Vehicular Technology Conference, pp. 549–553 (1991)
Dubslaff, C., Klppelholz, S., Baier, C.: Probabilistic model checking for energy analysis in software product lines. In: Proceedings of the 13th International Conference on Modularity, pp. 169–180. ACM (2014)
Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of Bluetooth device discovery. Int. J. STTT 8(6), 621–632 (2006)
Ghaderi, M., Boutaba, R.: Call admission control in mobile cellular networks: a comprehensive survey. Wirel. Commun. Mob. Comput. 6, 69–93 (2006)
Haverkort, B., Cloth, L., Hermanns, H., Katoen, J.P., Baier, E.C.: Model checking performability properties. In: Proceedings of DSN. IEEE CS Press (2002)
Kulkarni, V.G.: Modeling and Analysis of Stochastic Systems. Chapman & Hall, London (1995)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_47
Wang, J., Qiu, Y.: A new call admission control strategy for LTE femtocell networks. In: International Conference on Advances in Computer Science and Engineering, Sydney (2013)
Yang, X., Feng, G., Siew, C.K.: Call admission control for multi-service wireless networks with bandwidth asymmetry between uplink and downlink. IEEE Trans. Veh. Technol. 55, 360–368 (2006)
Zarai, F., Ben Ali, K., Obaidat, M.S., Kamoun, L.: Adaptive call admission control in 3GPP LTE networks. Int. J. Commun. Syst. 27(10), 1522–1534 (2014). Wiley
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Younes, S., Benmbarek, M. (2017). Performance Analysis of Multi-services Call Admission Control in Cellular Network Using Probabilistic Model Checking. In: Barkaoui, K., Boucheneb, H., Mili, A., Tahar, S. (eds) Verification and Evaluation of Computer and Communication Systems. VECoS 2017. Lecture Notes in Computer Science(), vol 10466. Springer, Cham. https://doi.org/10.1007/978-3-319-66176-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-66176-6_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66175-9
Online ISBN: 978-3-319-66176-6
eBook Packages: Computer ScienceComputer Science (R0)