中国铁路进入了跨越式大发展时期,当前正在研究的是基于GSM-R无线通信系统的车-地双向信息传输的CTCS-3级列控系统,它可以极大的提高铁路运输的安全性、可靠性以及运输效率。无线闭塞中心RBC(Radio Block Center)是CTCS-3级列控系统的地面核心设备,它通过计算并向列车发送运行许可来完成安全控车。因此,设计合理的行车许可的算法尤为重要。本文研究的主要内容是MA(Movement Authority)的算法原理、功能需求和实现,对MA进行模块划分,基于安全状态机理论对MA进行建模与分析,并且利用实时系统检验工具UPPAAL仿真并模拟安全状态机模型,最后对模型进行检验,说明MA算法的正确性。以下是论文完成的主要工作:一、首先从RBC的功能与接口入手,对MA的基本含义,功能需求以及算法原理进行了详细的分析和阐述。基于MA的功能需求,对其进行功能模块的划分,包括完全监控模式下的MA计算,引导模式下的MA计算,等级转换场景中的MA计算,相邻RBC交接的混合MA计算,包含临时限速信息的MA计算以及MA的管理功能,并且对各个功能模块的实现做出分析和设计;二、然后基于MA算法的原理,对MA进行结构化的模块划分,分为五个模块,即串路径模块,列车定位模块,更新路径模块,MA计算模块,MA发送模块。论文针对这五个模块,采用安全状态机理论对其进行建模和研究,运用安全状态机分层结构,并发控制,优先级控制这三个重要特征,结合状态抽象及转移条件控制,实现各模块的逻辑功能以及在特定场景下的MA计算方法;三、最后论证了UPPAAL模拟安全状态机模型的合理性,并且基于UPPAAL对MA进行建模和模型检验,为MA应用软件设计提供了理论依据。论文的创新点在于提出行车许可的算法,探索利用安全状态机理论,为RBC系统的行车许可模块进行建模与分析,提出行车许可的设计方案,并且用基于时间自动机的模型检验工具UPPAAL对安全状态机模型进行验证。安全状态机模型界面友好,可操作性强,进而可以展望推广到利用安全状态机为整个RBC系统进行建模与分析,为系统设计提供有力的依据。