The CTCS-3 train control system has high safety requirements, train control on-board equipment is the core of the CTCS-3 train control system. Its main function is to operate and control the train, which is the key to ensure the safety of train operation. Analyzes the information interaction between CTCS-3 train control on-board devices and the work mode conversion rules in the on-boar safety computer, Colored Petri Nets (CPN) were used to establish the information interaction model and work mode transformation model of on-board equipment. The ASK-CTL branching sequence logic formula was used to verify the dead identification, deadlock and transferability of the model under the working mode. It is proved that the CPN model constructed conforms to the process and rules of the system specification requirements, which can provide some reference for the design of the relevant security demanding system.