Formalization Model and Safety Analyses of High Speed Train in CTCS-3 Control Mode

China has established its railway technique system and engineering standard through technique importing, absorbing and recreation after recent ten years development. Several technique indexes of high speed railway of China have reached advanced level in the world. The mode of level 3 of Chinese Train Control System´ (CTCS-3) which used in Wuguang and Jinghu high speed railway will be the main control mode for high speed train in China. In order to find the factor of danger and provide mathematic foundation for improving this train control mode, it is necessary to establish formal model of this train control mode for researching the relationship among every key component and analyzing the reliability from abstract view. A formalization model of CTCS-3 train control mode was established based on Duration Calculus and Communicating Sequential Process and its reliability of train control process by CTCS-3 was analyzed through this model.