Formal Modeling and Verification of RBC Handover of ETCS Using Differential Dynamic Logic

The RBC (Radio Block Center) handover is an important part of European Train Control System level 2 which is a typical safety-critical hybrid system. In this paper, we build a formal model of RBC handover procedure using Differential Dynamic Logic, which is a first-order dynamic logic for specifying and verifying hybrid systems, and identify some constraints that are necessary for ensuring safety of train control, including collision avoidance as well as derailment avoidance. Moreover, we formally verify the safety-related properties of our model with deductive verification tool KeYmaera. The experimental results show the validity and feasibility of the method. Meanwhile, the safety constraints and safety-related properties verified in the paper can be helpful to the practical application of train control.