Title: A statistical model checking approach to analyse the random access protocol

Authors: Ahmed Roumane; Bouabdellah Kechar

Addresses: LaRATIC Laboratory, Ecole Nationale des Télécommunications et des Technologies de l'Information et de la Communication (ENSTTIC) Oran, Algeria ' Laboratory of Industrial Computing and Networking (RIIR), University of Oran1-Ahmed Benbella, Oran, Algeria

Abstract: 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.

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

DOI: 10.1504/IJWMC.2022.127603

International Journal of Wireless and Mobile Computing, 2022 Vol.23 No.3/4, pp.338 - 349

Accepted: 19 Jul 2022
Published online: 12 Dec 2022 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article