随着城轨CBTC(Communication Based Train Control,基于通信的列车运行控制)信号系统的发展以及5G(5th Generation Mobile Networks,第5代移动通信网络)技术的应用,基于车车通信的列车运行控制系统研究应运而生。该系统突破了传统CBTC系统以地面设备为核心的列车控制方式,重组系统架构,优化系统功能,以车载设备为核心实现移动闭塞功能,提高了列车的灵活性与智能性,同时由于地面设备的精简,使得系统间接口得到简化,控制信息直达列车,降低了系统反应时间。车载移动闭塞功能作为车车通信列控系统的核心功能,其正确性与有效性必须得到保障。形式化验证与仿真测试验证可以对系统规范制定的合理性以及系统功能实现的有效性进行验证,可及时发现系统开发过程中可能存在的不安全因素,对系统的研究和应用具有理论价值与实践意义。本文以车车通信列控系统架构为基础,重点研究实现系统车载移动闭塞功能的三大主要功能——前车识别、列车筛选以及车载移动授权生成,采用时间自动机理论和UPPAAL工具对上述功能的具体实现进行了形式化描述与验证,并在测试平台上完成了测试验证,验证了系统功能开发的合理性与有效性。具体工作如下:(1)在分析车车通信列控系统功能与特点的基础上,重点研究车载子系统移动闭塞功能。分析实现车载移动闭塞功能的主要模块的功能需求,分析前车识别、列车筛选以及车载移动授权生成过程中系统模块完成的具体功能及处理流程,并对各模块功能实现过程中子系统模块间的信息交互情况进行了分析,为后续系统的建模与验证奠定了基础。(2)根据列控系统VV&A(Verification,Validation,Accreditation,校核、验证与确认)理论与时间自动机建模过程,结合前车识别、列车筛选以及车载移动授权生成流程和系统模块间信息交互情况,分别建立了前车识别、列车筛选和车载移动授权生成模块时间自动机网络模型。采用UPPAAL工具依据的BNF(Backus-Naur Form,巴科斯范式)验证语法对各模块的安全性与受限活性特性进行了描述,并完成了相关验证。(3)搭建车车通信列控系统仿真测试平台,设计前车识别、列车筛选以及车载移动授权生成模块测试用例,依据测试用例及测试执行流程进行测试验证,完成了系统功能测试验证。