临时限速系统是高铁列控系统的核心构成之一,临时限速系统的工作流程严格依照客运专线列控系统临时限速技术规范来实现。技术规范中规定临时限速分为计划性限速和突发性限速,其两者都具有严格的时间逻辑关系和时间约束特性。技术规范的制定和执行都存在一定的人为因素干扰,为了保证铁路系统运营的安全和效率需要对技术规范进行合理的优化管理。临时限速系统作为高铁列控系统安全保障的核心环节,其安全性和受限活性受到运营场景的限制。因此运用形式化的分析方法对系统流程、发生事件和逻辑时间关系进行形式化分析和建模描述,验证系统在逻辑上的安全性和时间变化上的受限活性满足高铁列控系统的正确性要求。从而发现形式化描述的临时限速系统存在定义上的二义性和不可达性,找出系统中存在的缺陷为后续临时限速系统的优化和深层次的开发提供重要的理论验证依据。本文通过分析临时限速命令拟定校验、下达和执行反馈等基本操作流程,同时结合信息之间的交互关系和交互方式,并利用时间自动机理论可以建立三部分的时间自动机网络模型:非跨界临时限速时间自动机模型、跨界临时限速时间自动机模型和TSRS(Temporary Speed Restriction Server,临时限速服务器)切换与RBC(Radio Block Center,无线闭塞中心)切换重叠区域临时限速交互流程的时间自动机模型。这三个不同特殊场景下的时间自动机网络模型描述了系统临时限速命令的交互流程,根据系统要求的实时性和可达性设置不同的时间参数。根据上述时间自动机模型的规范描述和技术规范的要求,应用形式化BNF(Backus Normal Form,巴科斯范式)语法描述不同场景下时间自动机模型的验证语句,并将BNF验证语句输入到验证工具UPPAAL中对系统的安全性和受限活性进行验证,同时找出不满足临时限速系统受限活性要求的BNF语句对其中涉及到的时间约束变量进行分析,并给出解决方案。验证结果表明:根据系统建立的时间自动机模型满足其安全性要求,同时其受限活性中的时间参数变量指出临时限速技术规范中的不足。