Abstract: Focusing on the problem that the safety of CBTC computer based interlocking is critical, this article introduced the theory of timed automata, analyzed the architecture and differences between CBTC computer based interlocking system and traditional interlocking system, took an example of switch transaction, switch transaction model was established by using UPPAAL. The security requirements of the model were also analyzed, which showed the feasibility and effectiveness of the modeling and verification methods based on timed automata, during the process of developing computer based interlocking system.