%0 Journal Article %A DONG Jian %A DAI Shenghua %T Modeling and formal analysis of level transition based on colored Petri nets %D 2018 %R 10.3778/j.issn.1002-8331.1607-0240 %J Computer Engineering and Applications %P 208-213 %V 54 %N 2 %X In the process of high-speed train running, the time spent in the level transition of train control system and the success rate of the level transition seriously influence the safety of train operation and traffic efficiency. Level transition between CTCS-2 and CTCS-3 and level transition under degraded scenarios caused by typical equipment failures are modeled on colored Petri nets respectively, which models the information exchange between Radio Block Center(RBC), on-board equipment and fixed balises. This paper analyzes the influence of the speed of the train to the efficiency and the success rate of level transition, and the situation in the failure downgrade. The result shows that the models meet the requirements of safety and compatibility of CTCS-3 train control system. %U http://cea.ceaj.org/EN/10.3778/j.issn.1002-8331.1607-0240