基于无线通信的列车控制系统(CBTC)是我国城市轨道交通发展的一个重要方向,是国内正在研究的先进列车控制技术。Petri网建模理论是近年来快速发展的一种形式化建模理论。有色Petri网(CPN)结合传统Petri网的特征和高级编程语言的优势,以其图形化、直观的表示、良好语法、语义和强大的分析验证功能在很多领域都得到广泛的应用。本文在分析了基于无线通信的列车控制系统基本原理、结构的基础上,重点介绍区域控制器子系统(ZC)原理、功能,特别是区域控制器子系统切换的重要过程。本文采用具有严格数学定义的形式化建模语言CPN和相应工具CPN Tools对系统进行研究。对CBTC区域控制器子系统进行建模,通过仿真、验证来分析系统的正确性。采用分层Petri网对系统的上层模型进行描述,结合并发图理论和系统的状态空间生成报告对系统的稳定性、功能的正确性进行分析;用赋时网对切换信息交互过程的网络传输性能,系统响应时间,网络延时决定的信息传输时间的不确定性进行分析,最后得出系统在最坏的状况下可以安全切换的结论。