原文传递
基于模型检验的RBC子系统测试分析方法研究
| 论文题名： | 基于模型检验的RBC子系统测试分析方法研究 |
| 关键词： | 模型检验;RBC子系统;列车运行控制系统;UPPAAL建模 |
| 摘要： | CTCS-3级列车运行控制系统是采用铁路专用的移动通信系统GSM-R来实现车-地信息的双向传输过程，其中无线闭塞中心(RBC)负责生成行车许可(Movement Authority)并在CTCS-3级下进行控车，RBC子系统是CTCS-3级互联互通测试平台的一个组成部分，在整个控车流程中起着决定性的作用。RBC子系统测试分析的主体工作是发现在执行一个测试序列的过程中出现的异常，并找出导致该异常的原因，能够进行自动分析，是目前亟需解决的问题。 本文研究的主体是车载设备互联互通测试中的RBC子系统的测试分析，目的是实现分析自动化。测试对象是对RBC的控车流程进行功能性的验证，验证车载设备在RBC的控制下反应。当测试完毕之后，ATP会出现某些故障反应，在出具报告时需要说明ATP出现某个故障反应的原因。解决上述问题的根本在于找到引起故障发生的一连串相关的状态迁移的一个集合，这个集合既为整个测试过程中的功能状态点，整个测试过程从开始到结束，可以看作为随着时间迁移的离散的状态点集合，故障反应及故障反应相关联的状态均包含在此集合中。在确定要分析的故障状态A后，寻找与其相关联的状态，即寻找引起这个故障状态A的原因R，在数学层面上即为检测是否存在一个可执行序列从状态R到达状态A，即可达性分析。 本文的主要工作为以追溯引起测试过程中出现异常状态的原因为例，深入分析了基于模型检验的RBC子系统测试分析方法。首先从形式化建模方法作为切入点，来寻找反映整个RBC子系统行为的方法，其次作者使用UPPAAL建模工具对RBC子系统的控车流程建立了时间自动机模型，并创新性的通过对UPPAAL中间过程文件XML进行解析，实现了非开源的UPPAAL建模软件与实际测试平台之间的数据通信，采用模型检验的方法对所建立的模型进行可达性分析，一定程度上实现了自动测试。并将上述研究成果落实到软件实现层面，完成了分析工具的开发工作，在与整个测试平台进行联调联试后，证明文中所提出的方法具有一定的可行性，为以后的进一步完善测试平台做出来一定的贡献。 |
| 作者： | 宋海锋 |
| 专业： | 交通信息工程及控制 |
| 导师： | 唐涛 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2014 |
| 正文语种： | 中文 |
检索历史
应用推荐
