随着通信技术的发展,为改善基于通信的列车控制系统（Communication Based Train Control,CBTC）,基于车车通信的列控系统成为下一代城市轨道交通列控系统的主要发展方向。基于车车通信的列控系统是在CBTC列控系统的基础上,将部分地面设备功能转移到车载设备上,优化了系统结构,实现了以车载为核心的控制理念。作为一种新的列控系统,在投入使用前进行形式化的建模验证与仿真测试必不可少,可以提前发现系统中可能存在的设计缺陷,保证系统满足安全性、功能性和性能性的要求,对系统的研究与应用有重要意义。本文以车车通信列控系统为研究对象,主要工作如下:（1）分析新型列控系统的结构和特点,重点选取了新型列控系统中的新增功能和功能分配发生改变的模块,主要包括列车站内选路、前车识别、移动授权生成三个功能模块,分析各功能的具体实现流程和各设备之间的信息交互情况,并根据车车通信列控系统的特点,提出了适用于车车通信列控系统的后备模式,描述了列车在车车通信故障情况下切换为后备模式的过程。（2）通过对比分析各形式化建模方法的特点与优劣,选取有色Petri网理论,根据“自顶向下”分层建模的思想,建立了各项功能的层次赋时有色Petri网模型,利用CPN Tools工具完成了模型的功能验证和状态空间性质分析,通过模型的状态空间报告验证了模型能满足可达性、有界性、活性和公平性的要求,并通过仿真分析得出了列车故障情况下后备模式切换的成功率,对能够成功切换后备模式的列车分析,得到列车后备模式切换所需时间与切换成功后可运行时间分布图。（3）在形式化建模的基础上,在Visual Studio 2013的环境下开发了基于车车通信列控系统的仿真软件,通过对仿真软件的需求分析和结构设计,完成了新型列控系统仿真软件的开发,并设计了相应的测试案例,仿真软件可通过输入具体的线路参数、列车数据、故障情况等信息模拟列车在尽可能真实情况下的运行状态,进一步表明所设计的列控系统方案的可行性。结果表明,所建立的功能模型能有效满足车车通信列控系统的功能性需求与安全性需求,可为车车通信列控系统的建模与分析提供一定参考。