| With the development of science and technology and increased automation, the mode of urban rail transit system in world is also changing. As a new concept, advanced urban passenger traffic mode, Fully Automatic Operation (FAO) system represents a new urban rail transit development direction. However, safety integrity level of FAO system is four, and reliability index is higher than99.99%. Therefore, some control vehicles need to be considered redundant structure. As a non-fault vehicle, Automatic Train Operation (ATO) system on-board is urgent to design for reliability and security.In this paper, ATO on-board in FAO system is the research object. Combined with overall requirements analysis for ATO and Byzantine fault tolerance theory, Quadruple Modular Redundant (QMR) system for ATO is given in detail, to ensure ATO system has high reliability and high security.Based on IEEE1588which is a precision clock synchronization protocol, an improved high precision clock synchronization method is introduced to solve distributed system clock synchronization. With the use of handshake mechanisms and data processing, weaken the influence of various factors, QMR system for ATO can achieve sub-millisecond accuracy.Data consistency protocol is introduced to solve the input and output consistency of QMR system. With two rounds of information exchange, it can achieve coherence between the four channels to ensure the system can tolerate one Byzantine fault.Symbolic Model Verification (SMV) is introduced as a symbolic model checking tool. Clock synchronization method and Data consistency protocol are verified with SMV in the paper. It is proved that the safety of the model and the correctness of the design by the result of formal verification.Finally, in the laboratory environment, a simulation and test system is build to test the basis function of ATO redundant system. According to test results, it shows that the design of ATO redundant system in the paper is feasible and workable. |