Modeling and Verification of Inter-Station Section Direction Control Function Applicable to TBTC and CBTC

In the process of requirement analysis of Interstation Section Direction Control function applicable to TBTC and CBTC, to prevent the introduction of inherent safety defects due to misunderstanding of requirements. The formal method is used to improve the accuracy of describing the functional requirements of Inter-station Section Direction Control, enhance the rationality of design, and reduce the risk of introducing safety defects. First, the EVENT-B language model of each layer is established by using state transition diagram and refinement strategy, and the safety characteristics of the system are verified by proving the invariant proof obligation. Through the accuracy and hierarchy of the formal modeling process and the corresponding verification activities, it is proved that the method is feasible and efficient.