Modeling And Analysis Of RBC Handover Based On Timed RAISE

Chinese train control system(CTCS) is the important equipment to control the safe operation of trains and improve the efficiency of train traffic in China railway. Radio block center(RBC) is an important part of CTCS-3 train control system, RBC handover affect the safety and efficient operation of the train. Train control system is a complex safety-critical system, both in the making process of standards and norms and in the development and design phase of the system, there are inevitably some vulnerabilities or security risks. Therefore, the use of formal methods for RBC handover protocol modeling and verification is essential.The formal verification methods used at this stage are mostly based on model checking. Because formal method based theorem proving is able to describe systems with infinite state space, in contrast, it is more suitable for more complex structure of train control systems. Formal method based theorem proving currently is used only for a particular characteristic of the train control system, and it is difficult to fully describe the model for validating system. Therefore, this thesis uses formal methods timed rigorous approach to industrial software engineering(Timed RAISE) to model RBC handover protocol of CTCS-3 train control system specification and to verify the correctness and real time of system model.Firstly, the Timed RAISE method is introduced. The basic concepts, modeling and validated methods of RAISE specification language(RSL) are described by a concrete example, and the inference rules used in model validation are analyzed.Secondly, the thesis analyzes the RBC handover procedure, and establishes interactive information photograph based on the process of information transmission between devices. The domain model of RBC handover is established by using the domain method, and in the domain model, a state transition diagram is constructed by the entire continuous process into discrete processes in time. Combined with the description of interactive information figure for the information exchange process, model state transition diagram is described formal by using RSL, and RSL model of RBC handover protocol is established.Finally, the correctness requirements and time constraints of RBC handover protocol is analyzed, the correctness and real time of handover protocol is described by using RSL. RSL model is inferred and verified by using inference rules, the results show that RBC handover protocol meet the correctness and real time requirements of standard specification. Compare validation results and conclusions other literature, shows that the method is universal, at the same time a reasonable suggestions for handover protocols is given.