原文传递
基于UPPAAL的CBTC系统数据验证的研究
| 论文题名： | 基于UPPAAL的CBTC系统数据验证的研究 |
| 关键词： | CBTC系统;列车运行安全;运输效率;数据验证;流程设计 |
| 摘要： | 基于通信的列车控制（Communication Based Train Control，CBTC）系统是保证列车运行安全、提高运输效率的安全苛求系统。CBTC各子系统依靠配置数据来定义系统的功能，数据作为系统核心组成部分，其正确性是CBTC系统安全连续运行的重要保证，如何保证数据的正确性，寻找一种有效的研究方法对整个CBTC系统具有非常重要的意义。基于严格数学定义的形式化方法不仅能精确、清晰地描述系统结构和相关特性，而且能对特性进行验证，本文采用形式化的方法对CBTC系统数据进行验证，以此来保证系统数据的正确性。 首先，论文分析了CBTC系统结构组成与数据特点，根据安全苛求系统和CBTC系统的具体需求，结合时间自动机理论和模型分析验证工具UPPAAL，提出了基于UPPAAL的CBTC系统数据验证的方法，并设计了CBTC系统数据验证的具体建模方法和验证流程。 然后，论文在前述理论基础和流程设计的基础上，按照CBTC系统数据的形式化验证机制，先后对CBTC系统的数据组成与描述方式进行了分析和深入研究。围绕CBTC系统数据的性质和特点，总结了CBTC系统所需的基础线路数据、轨旁设备数据以及区域功能数据，得到CBTC系统数据验证的策略，从值域关系、参照关系和逻辑关系三个角度建立了数据约束集合，并根据这些数据约束条件对CBTC系统数据验证体系进行建模，形成一种数据的自动化验证方法。先将系统数据抽象成带有状态的时间自动机模型，然后把数据约束条件以数学公式和逻辑语言的方式加以描述，并针对CBTC系统数据进行验证的结果进行分析。 最后，论文针对北京地铁亦庄线的实际数据，运用时间自动机理论和模型验证工具UPPAAL，根据不同的系统数据和数据约束条件，通过分层递进的方式对数据进行了建模和形式化验证。结果表明，基于UPPAAL的CBTC系统数据验证方法具有一定的可行性和可用性。 |
| 作者： | 王森 |
| 专业： | 交通信息工程及控制 |
| 导师： | 黄友能 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2013 |
| 正文语种： | 中文 |
检索历史
应用推荐
