原文传递
基于统计模型检测的TcCBTC系统建模与安全分析
| 论文题名： | 基于统计模型检测的TcCBTC系统建模与安全分析 |
| 关键词： | 城市轨道交通;列控系统;统计模型检测;安全分析 |
| 摘要： | 随着列控技术的快速发展以及人们出行需求的增加，城市轨道交通正在朝着高智能、高密度、高安全等目标迈进。各国研究人员积极开展新型列控系统的研发工作，其中以车载为核心的CBTC(Train-centric Communication Based Train Control,TcCBTC)系统成为研究热点，其采用车车通信技术简化了控制信息的交互环节，通过对列控功能的再分配实现系统结构的优化，提升了车载的智能化程度，降低了全生命周期成本。目前TcCBTC系统正处于核心技术突破和样机研制阶段，系统运行过程中的不确定性行为可能影响行车安全。因此，系统在投入使用前必须经过严格的安全验证，以确保系统的安全高效运行。本文以随机混成自动机(StochasticHybridAutomata,SHA)理论作为建模基础，以统计模型检测(StatisticalModelChecking,SMC)作为安全分析基础，提出了TcCBTC系统形式化建模与安全分析框架。在此基础上，通过UPPAAL-SMC对选取的实例进行分析，验证了方法的有效性，研究工作如下： (1)介绍了TcCBTC系统的国内外研究现状，深入分析了TcCBTC系统的结构、各子系统功能。建立TcCBTC系统的结构参考模型，对系统的通信接口以及各子系统通过接口交互的信息进行了分析。采用基于模型的方法结合HAZOP-Ⅰ方法对系统运行过程中的风险进行辨识，即分析系统运行的不确定环境，为后续建模提供基础。 (2)分析了列控系统形式化建模和验证方法的研究现状，对基于模型的安全分析方法、模型检测技术作了简要阐述。针对TcCBTC系统所处运行环境的不确定性，提出基于SHA的形式化建模方法，实现对系统运行时的混成行为和随机行为的刻画。利用DMTL语义描述所验证的性质，通过UPPAAL-SMC建立系统的形式化模型，并基于统计模型检测的思想对TcCBTC系统进行安全性分析。 (3)针对TcCBTC系统运行场景进行实例研究。以移动授权场景和列车区间追踪为例，分析了各场景下系统的功能需求，确定参与此过程的子系统及其交互信息和系统运行中的不确定因素。然后，建立包含系统不确定运行环境的SHA网络模型，在静态环境中验证所建模型符合系统功能属性需求的基础上，基于SMC算法在UPPAAL-SMC中对系统模型进行定量分析。验证了不确定因素对系统的影响，并通过拟合得到对应量化指标下参数的可行域，实现对列车状态的实时监控，提高系统安全性。 |
| 作者： | 闵晓琴 |
| 专业： | 交通信息工程及控制 |
| 导师： | 林俊亭 |
| 授予学位： | 硕士 |
| 授予学位单位： | 兰州交通大学 |
| 学位年度： | 2022 |
检索历史
应用推荐
