Modeling and Verification of RBC Handover Protocol

Radio Block Center (RBC) is a core part of the Chinese Train Control System level 3 (CTCS-3) which is a protocol for safety critical systems. The correctness of the RBC handover protocol is one of the most important factors affecting the safety of systems. Hence, it is of great importance to ensure the correctness of the protocol. To this end, some formal methods have been used to model and verify the protocol. In this paper, we use Modeling, Simulation and Verification Language (MSVL) as the formal language to model and verify the protocol. The result shows that the behavior of RBC handover is consistent with the specification.