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