A statistical model checking approach to analyse the random access protocol

被引：0

作者：

Roumane A. ^{[1
]}

Kechar B. ^{[2
]}

机构：

[1] LaRATIC Laboratory, Ecole Nationale des Télécommunications et des Technologies de l'Information et de la Communication (ENSTTIC), Oran

[2] Laboratory of Industrial Computing and Networking (RIIR), University of Oran1-Ahmed Benbella, Oran

来源：

International Journal of Wireless and Mobile Computing | 2022年 / 23卷 / 3-4期

关键词：

cellular network; formal verification; mobile network; model checking; random access procedure; statistical model checking;

D O I：

10.1504/ijwmc.2022.127603

中图分类号：

学科分类号：

摘要：

Mobile cellular networks are becoming the most important technology in the telecom industry, and this made them a preferred subject for research and development of new hardware and software systems. In order to check the validity of these systems, one can use either a simulation or formal methods. Recently, new emerging methods have been proposed as alternative solutions, such as Statistical Model Checking (SMC). In this paper, we present a comprehensive framework based on SMC that could be used to analyse the cellular network protocol Random-Access Procedure (RAP), by using UPPAAL. We model the system using a simplified network of timed automata, we check the validity of our model by running some concrete simulations and after that we perform a formal verification of some properties of the protocol. Finally, the statistical approach, SMC, is used to study the performance of the system. Copyright © 2022 Inderscience Enterprises Ltd.

引用

页码：338 / 349

页数：11

共 39 条

[1]

Abdelhamid M., Atallah A., Ammar M., Mohamed O.A., Reliability analysis of autonomous UAV communication using statistical model checking, Proceedings of the IEEE International Midwest Symposium on Circuits and Systems (MWSCAS), pp. 340-343, (2021)

[2]

Althumali H.D., Othman M., Noordin N.K., Hanapi Z.M., Dynamic backoff collision resolution for massive M2M random access in cellular IoT networks, IEEE Access, 8, pp. 201345-201359, (2020)

[3]

Amirsaidov U.B., Qodirov A.A., Implementation of the reinforcement learning mechanism in the random access channel procedure, Proceedings of the IEEE 14th International Conference on Application of Information and Communication Technologies (AICT), pp. 1-5, (2020)

[4]

Arora S., Rathor A., Rao M.V., Statistical model checking of opportunistic network protocols, Proceedings of the Asian Internet Engineering Conference, pp. 62-68, (2015)

[5]

Baier C., Katoen J., Principles of Model Checking, (2008)

[6]

Basile D., Ter Beek M.H., Ciancia V., Statistical model checking of a moving block railway signalling scenario with Uppaal SMC, International Symposium on Leveraging Applications of Formal Methods, pp. 372-391, (2018)

[7]

Boyer B., Corre K., Legay A., Sedwards S., PLASMA-lab: a flexible, distributable statistical model checking library, Proceedings of the International Conference on Quantitative Evaluation of Systems, pp. 160-164, (2013)

[8]

Copeta P.B., Marchettoa G., Sistoa R., Costab L., Formal verification of LTE-UMTS handover procedures, IEEE Symposium on Computers and Communication (ISCC), pp. 738-744, (2015)

[9]

Copeta P.B., Marchettoa G., Sistoa R., Costab L., Formal verification of LTE-UMTS and LTE-LTE handover procedures, Computer Standards and Interfaces, 50, pp. 92-106, (2017)

[10]

Gamatie A., Sassatelli G., Mikucionis M., Modeling and analysis for energy-driven computing using statistical model-checking, Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 980-985, (2021)

← 1 2 3 4 →