随着我国铁路系统的迅速发展,高速列车在我国进入了相应的快速发展期。车站列控中心(TCC)是CTCS-2级列控系统地面核心设备,在CTCS-3级系统中也是不可缺少的后备设备。它根据轨道电路状态、车站联锁系统、临时限速命令等信息,生成并传输相关控车指令,保证在当前列控中心管辖范围内的列车的安全。列控中心软件的可靠性和实时性对整个系统的安全运营尤为重要。为了在实验室环境下搭建"CTCS-3级虚拟仿真实验系统",设计合理、可靠的列控中心软件,本文对列控中心系统做了如下研究:首先,系统的研究了 CTCS-2级列控系统中列控中心的结构、功能和系统接口,选取其有源应答器报文编制功能和轨道电路编码功能作为主要研究对象,为模型设计做铺垫。其次,对目前典型的形式化方法做了研究,通过比较不同方法的适用领域,并结合列控系统的特点,选用时间自动机理论作为列控中心控车流程的研究方法,并对其建模与验证工具UPPAAL做了相关介绍。再次,根据列控中心系统的特点与技术指标,分析其轨道电路编码与有源应答器报文编制的工作流程。结合时间自动机理论,在前人的研究基础上,对有源应答器编码流程进行基于场景的分层设计,建立了 6层网络结构,分别设计成员时间自动机;通过使用通道和设置全局变量,在模型验证工具UPPAAL中构建时间自动机网络;使用仿真器和验证器对其功能和性能进行仿真和测试,结果表明改进的模型对列控中心的通信流程以及编码流程描述的更加准确,降低了系统中存在的主观因素。最后,依据《列控中心技术指标》和实验室环境,采用C#软件与数据库技术,对列控中心软件进行模块化设计,通过基于场景的编码算法,实现了能根据轨道占用情况、联锁系统和临时限速服务器命令生成全线轨道电路低频编码和有源应答器报文的列控中心软件,并对软件运行效果进行相应展示,满足了实验系统的需求。