与航空、公路等交通方式相比,铁路运输具有运量大、环境友好、准点率高等优点,使得铁路运输在各国交通运输体系中占有重要的地位。列车运行控制系统是铁路信号的重要组成部分,是保障行车安全、提高运输效率和行车速度的关键子系统。随着我国"一带一路"的战略的实施,如何满足互联互通需求和安全技术保障成为了铁路信号领域所关注的问题。ETCS是为实现互联互通而制定的列控技术规范,其中ETCS-1级与ETCS-NTC级之间的等级转换是欧洲列控系统和本国列控系统之间的转换,因此对两者之间等级转换的研究非常有必要。通过形式化模型对系统进行设计和验证,可以保证系统设计开发的正确性和安全性。本文在对ETCS系统需求规范、专用传输模块接口规范、互联互通性能要求规范进行需求分析的基础上,建立了 ETCS-1/ETCS-NTC等级转换的列控车载设备、轨旁单元和系统环境间信息交互的时间自动机模型,最后对模型进行仿真和形式化验证。首先,从系统功能架构和系统应用等级方面对ETCS进行了介绍,阐述了 ETCS的适用范围、系统组成、系统环境和应用现状。其次,对列控车载设备从开始任务进入ETCS-1级、到与专用传输模块连接,ETCS-1级向ETCS-NTC级转换,ETCS-NTC级向ETCS-1级转换的的场景进行详细分析,对这几个场景中涉及到的列控车载设备、地面应答器和司机建立独立的时间自动机模型。最后,将这几个场景里所建立的各个独立的时间自动机子模型组成系统的时间自动机网络模型,通过UPPAAL验证工具对网络模型进行仿真,并用巴科斯范式语句对网络模型进行形式化验证,最终达到验证模型的目的,证明了所建立的模型能够满足系统性能要求,为列控系统的设计提供了参考。