Formal Approaches to Mode Conversion and Positioning for Vehicle System

The mode conversion and positioning of the vehicle subsystem of the Communication Based Train Control System (CBTC), need to be safe and reliable, being two critical components. To meet this requirement, we apply formal methods in the design of rail transport systems. This paper studies the specification and verification of the mode conversion and positioning system. The mode conversion system is studied by using Communicating Sequential Processes (CSP) combined with simple data structure. The positioning system is explored by combining CSP with Object-Z (OZ). Based on the achieved model, the safety property verification and simulation are proceeded by the automatic process analysis toolkit PAT.