Abstract: The high speed train control system is a core equipment, which plays an important role in assuring safety and improving efficiency in railway. How to verify the correctness of the functions of system in order to improve the safety is especially important. In this article, the process calculus based method called hybrid communication sequential process(HCSP) was introduced. The formal description to the train control system was taken by HCSP. For typical scenarios, the scenarios of registration and start up were modeled by HCSP. By introducing transition rules, the corresponding model transformation was carried out. The model checking tool UPPAAL was used to simulate and verify the function. The results showed that the model was correct and the method was feasible.