随着通信技术特别是无线电通信技术的快速发展,CBTC (Communication-Based Train Control,基于通信的列车运行控制)系统应运而生,并在城市轨道交通中得到广泛应用。CBTC系统实现了列车与地面设备间的大容量双向连续信息传输,能够对列车实施精确的列车控制,显著提高了行车效率和运输能力,同时大大减少了轨旁设备,节省了成本和维护费用。在CBTC系统中,移动授权的分配和执行是整个CBTC系统的核心,CBTC的子系统区域控制器(Zone Controller,ZC)承担着移动授权生成和分配的核心功能。列车追踪功能是ZC子系统核心安全功能之一,是生成和分配移动授权的基础。针对区域控制器列车追踪过程具有动态、并发、实时、交互等特点,本文采用层次时间有色Petri网(HTCPN)的形式化建模方法来对列车追踪进行建模,以模拟列车追踪的实现,分析其重要性质。并用CPN tools工具对模型进行仿真分析,以验证模型的正确性。HTCPN克服了普通Petri网的不足之处,既可以给出直观的列车追踪模型的顶层结构,并根据需要对模型进行不同程度的分层细化,又可以模拟出列车追踪过程的时序性,体现系统严格的时间机制,有利于对模型进行分析和仿真实现。本文首先描述了层次时间有色Petri网的相关理论知识,包括其定义、动态属性、分析方法以及建模工具。接着研究区域控制器的列车追踪功能,依照系统功能需求,从系统结构、所需信息的交互以及工作流程等多个角度详细阐述了列车追踪的原理。本文分析了利用HTCPN对区域控制器列车追踪建模的可行性,并构建了顶层、列车筛选处理层、列车追踪处理层及其各功能子层的三层模型。利用CPN Tools工具对系统模型进行仿真运行,观察列车追踪过程在模型中的体现以及信息的交互传递情况。在对模型进行仿真分析后,利用状态空间分析技术,通过状态空间可达图以及状态空间报告分别对系统功能和系统性质进行了验证,从不同角度验证了模型设计的合理性与数据传输的正确性,有助于构建更加完善的区域控制器系统模型,也为区域控制器系统软件的实现提供了理论依据。