随着各大城市城市轨道交通建设的加速发展，CBTC(Communication Based TrainControl，基于通信的列车运行控制)系统因其高可靠性、高安全性的优势已成为城市轨道交通的主要发展方向。人们对于列车运行的高速度、高安全性提出了更高的要求。ZC(Zone Controller，区域控制器)作为CBTC系统中保证列车安全运行的关键部分，它承担着市民安全出行的重大责任。而区域控制器是一个内部结构复杂且实时性很强的系统，其内部各项功能模块中出现的任何可能存在的设计缺陷都可能造成无法弥补的后果，为了更加及时、准确地找出系统中可能存在的缺陷，在对系统进行深层次开发的前期，利用形式化方法的优势，尽可能严谨、正确地描述系统结构体系和功能，并对其功能要求和性能要求进行验证对保障城市轨道交通运输安全具有重要意义。　　本文以区域控制子系统为研究对象，采用时间自动机理论和UPPAAL验证工具对ZC边界切换和列车追踪两大功能模块进行描述，并对系统的功能性和实时性要求进行验证。　　首先，介绍CBTC的基本构成、区域控制器的功能结构及CBTC中各子系统之间的信息交互过程，并对列车跨越ZC边界场景和列车追踪场景进行重点研究，深入分析ZC边界切换的实际情况和列车追踪处理的具体过程，为两个场景下区域控制器的建模验证奠定理论基础。　　其次，通过分析列车跨越ZC边界过程中，不同位置的具体操作，结合列车与两个区域控制器之间的信息交互关系，利用时间自动机理论建立了ZC边界切换时间自动机网络模型。通过分析列车追踪的具体处理过程，结合处理过程中区域控制器内部各模块之间的信息流向，利用时间自动机理论建立列车筛选、列车追踪分界点和同一区段内两列车追踪的时间自动机网络模型。　　最后，用BNF(Backus Normal Form，巴科斯范式)编译列车跨越ZC边界场景和列车追踪场景下区域控制器的功能性要求和性能要求，将得到的验证语句在UPPAAL验证器窗口中进行验证，实现了对两个场景下系统功能性和实时性的验证。为后续区域控制子系统性能的优化和深层次的开发，在设计开发前期提供理论参考。