原文传递
基于安全状态机的RBC系统行车许可模块的建模与验证
| 论文题名： | 基于安全状态机的RBC系统行车许可模块的建模与验证 |
| 关键词： | 安全状态机;行车许可模块;无线通信系统;铁路运输;无线闭塞中心;功能需求 |
| 摘要： | 中国铁路进入了跨越式大发展时期，当前正在研究的是基于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系统进行建模与分析，为系统设计提供有力的依据。 |
| 作者： | 耿鹏 |
| 专业： | 交通信息工程及控制 |
| 导师： | 邱宽民 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2009 |
| 正文语种： | 中文 |
检索历史
应用推荐
