CTCS-3级列车运行控制系统是我国引进、吸收然后再创新的列控系统,它极大的提高了高速列车的运行效率和安全性。RBC是CTCS-3级列控系统中的核心设备,由它生成行车许可命令能够保障列车顺畅运行。因此,分析RBC生成行车许可的流程并利用形式化方法建模和验证系统规范的正确性是十分必要的,本文采用时间自动机理论对CTCS-3级列控系统的三种场景下行车许可生成进行建模仿真和验证。在验证系统的实时性时,形式化方法是一种保障正确性和可靠性的重要途径。RBC是一种典型的实时系统,而时间自动机是专门为了研究实时系统的,它能够较完整的描述实时系统的时间特性,因此,本文选用时间自动机理论对RBC系统生成行车许可建模。模型的验证需要利用合适的实时系统模型验证工具,通过对比本文运用实时系统验证工具UPPAAL进行验证。论文依据《CTCS-3级列控系统总体技术方案》和《无线闭塞中心(RBC)技术规范》详细的分析了CTCS-3级列控系统行车许可生成、等级转换和RBC切换的流程,各设备之间的通信连接和信息交互过程。同时需要提取需要验证的功能属性和时间属性。在建模过程中,首先是确定建模对象,例如各种硬件设备;然后,根据研究对象之间的联系,提取抽象对象的行为和动作并映射为形式化语言;最后,确定模型的状态跳转路径和约束条件,得到相应的时间自动机模型。利用UPPAAL工具中对系统模型进行模拟,通过随机得到的仿真序列观察研究对象的信息通信和状态变化。同时,应用工具中的验证器验证了研究对象的功能属性和受限活性。论文完成了RBC生成行车许可的建模与验证。研究结果表明所建模型满足技术规范的功能属性和安全性要求。