Formal verification of a radio network random access protocol

Summary In this paper, the random access procedure of Universal Mobile Telecommunications System network is investigated. We have proposed a model based on communicating timed automata that represents the main functions related to the random access procedure including the user equipment, the base station (node B or BTS), and the channel. Then, we have used computational tree logic formula to specify the proprieties to be verified. The model and the formulas serve as inputs to the model checker, which is used as a verification engine, ie, UPPAAL and SPIN. The formal verification approach shows that the protocol has several drawbacks that may not be detected by simulation.