摘要 : 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 ... 展开 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. 收起