随着城市化脚步的逐渐加快,CBTC(Communications-Based Train Control,基于通信的列车控制)系统已经成为当今世界城市轨道交通列控系统的发展趋势。ZC(Zone Controller,区域控制器)作为CBTC系统的核心设备,是实现列车安全追踪的关键,其可靠性直接关系到列车是否能安全运行。为了及时并准确发现系统设计缺陷,在系统开发早期使用一种工具对系统进行描述和验证就显得尤为重要。形式化方法是以精确的数学语言分析和验证系统的技术和工具。本文采用形式化方法对ZC进行建模和验证,目的在于保证ZC设计的正确性和安全性。首先,论文分析了当前主流的形式化方法,根据安全苛求系统的设计要求,提出了形式化方法时间自动机理论及其自动验证工具UPPAAL。其次,在对CBTC的基本结构和运行原理进行分析的基础上,对本文的重点ZC的工作原理进行深入的分析,提出了系统的功能和性能需求。由于ZC是一个复杂实时系统,可将其按照功能划分为四大模块:列车管理、移动授权、ZC切换以及ZC与CBTC其他子系统信息交互。然后分别对它们的流程进行了设计。根据列车在CBTC区域运行的流程设计,利用时间自动机分别对ZC的功能进行建模,通过设置通道和共享变量实现几个时间自动机的通信,将其组成为一个完整的时间自动机网络模型。最后,利用UPPAAL对所建模型进行模拟得到消息序列图,分析了列车在CBTC区域运行过程中状态的变化以及各子系统间的通信。然后应用BNF语句提炼出系统的功能和性能需求,并成功地进行了验证。验证结果表明时间自动机的形式化方法对实时系统的分析和验证有一定的可行性,能够为CBTC的继续研究提供参考。