随着科学技术的发展以及自动化程度的提高,世界上城市轨道交通系统的运行模式也在发生变化。全自动无人驾驶系统作为一种全新理念的、先进的城市客运交通模式,它代表着城市轨道交通新的发展方向。然而,全自动驾驶系统的安全完善度等级为4,可靠性指标要高于99.99%。因此车辆上的一些控制系统设备需要考虑冗余。而车载ATO设备本身是非故障安全的,故根据需要,需要对车载ATO设备进行可靠性和安全性设计。本文以全自动无人驾驶系统中的ATO车载设备作为研究对象,引入拜占庭容错理论,并结合ATO系统的整体需求分析,给出了四余度ATO冗余系统的详细设计方案,来保证ATO系统的高可靠性和高安全性。论文引入IEEE1588时钟同步技术,提出一种改进的高精度时钟同步方法。通过握手机制和对测量数据的处理,有效减弱各种因素的影响,使得ATO冗余系统能够达到亚微秒级的时钟同步精度。引入数据一致性协议,解决ATO冗余系统的输入一致性、输出一致性的问题。通过两轮信息交换,来实现四个通道间的协调一致性,保证系统可以容忍一个拜占庭故障。引入符号模型检验工具SMV,对时钟同步算法和数据一致性协议建立模型,并进行形式化验证。通过验证结果和分析,证明了建立模型的安全性,以及设计方法的正确性。最后在实验室环境下,构造了一个模拟测试系统。针对ATO冗余系统的基本功能进行实验室模拟测试。根据测试结果,表明论文设计的ATO冗余系统是可行和有效的。本文共有图31幅,表13个,参考文献34篇。