众多工业控制领域要求其计算机控制系统具有高可靠、高可用和高安全的运行基础。安全计算机系统常用于军事、航空航天、工业控制、银行、通信等安全苛求(safety-critical)领域,以避免由于计算机的失效造成重大事故。基于通信的列车运行控制(Communications-Based Train Control, CBTC)系统是当今世界列车运行控制系统的发展趋势,各主要发达国家都相继开发出自己的CBTC系统。在CBTC系统中,地面区域控制中心的主要组成部分是区域控制器ZC以及数据存储单元DSU,其中ZC管辖区域中所有列车的车载控制器VOBC将列车所在位置和速度等信息发到安全计算机平台之上的ZC应用程序中,经过保证安全的计算后再将移动授权MA发往VOBC控制列车的下一步运行,而DSU子系统包括了其它列车控制子系统使用的所有数据库和配置文件,它的应用软件也需要搭建在安全计算机平台之上。二乘二取二冗余结构的安全计算机平台是提高系统安全性、可靠性的一种重要解决方式。CBTC列控系统的安全计算机平台采用二乘二取二冗余结构,它是一个实时系统,控制过程需要考虑时间因素。本文分析CBTC系统安全计算机平台系统的组成结构,提取出系统的功能约束,采用基于时间自动机理论的建模验证工具UPPAAL建立系统的自动机网络模型,进行仿真分析,验证系统的功能性、实时性、安全性要求。