摘要：基于通信的列车运行控制系统（ Communications-Based Train Control System, CBTC）相较于传统的基于轨道的列车运行控制系统,无论是从功能方面还是性能方面都有了很大的改进。在系统的研发过程中,对其进行建模和验证,能够发现系统设计的缺陷,进而保证系统的安全性和功能性。移动授权（ Movement Authority, MA）是CBTC系统的核心功能,用来保证列车的安全运行间隔。通过对移动授权生成原理的研究,采用时间自动机和其自动验证工具UPPAAL对其进行建模以及验证,验证结果表明,搭建的移动授权模型能够达到规定的安全要求和功能要求。因此UPPAAL能够对复杂的实时系统进行仿真验证。

关键词：cbtc ma 时间自动机 uppaal 

单位：兰州交通大学自动化与电气工程学院 兰州730070 兰州交通大学电子与信息工程学院 兰州730070