论文部分内容阅读
RBC(Radio Block Center,无线闭塞中心)作为CTCS-3级列控系统地面核心设备,围绕RBC的运营场景是列控系统主要的工作方式,在确保系统安全运营的过程中扮演着重要角色。CTCS-3级列控系统是多学科领域的融合与提升,列车的运行过程和相关设备间的离散信息交互相互影响,使RBC控车场景呈现显著的混成特性。CTCS-3级列控系统规范作为系统生命周期需求阶段的主要工作,是列控系统开发的前提和必要条件,其详细分析了为确保列车安全运行所必备的功能需求以及解决方案。对系统进行需求阶段的安全分析是系统安全设计和安全评估顺利进行的关键,对于保障系统的安全性具有重要意义。因此,以RBC控车场景——注册与启动、行车许可、等级转换、注销,作为研究对象,以系统混成性作为出发点,选取系统生命周期的需求阶段,以CTCS-3级列控系统规范作为研究依据,对RBC控车场景进行安全分析。采用UML(Unified Modeling Language,统一建模语言)与PHAVer(Polyhedral Hybrid Automaton Verifier,混成自动机模型检验工具)相结合的方法进行需求阶段的RBC控车场景的安全分析。首先,通过UML支持的扩展机制,对UML进行面向混成性的扩展,建立RBC控车场景UML模型,实现对RBC控车场景相关设备的离散信息交互过程以及连续动态演化过程,即混成性的描述。然后,依据CTCS-3级列控系统需求规范,分析RBC控车场景的基本功能需求,根据UML到PHAVer的转换规则,将UML模型转换成PHAVer模型,验证PHAVer模型的正确性。最后,通过分析RBC控车场景,找出各相关设备可能的功能模块故障情况,建立RBC控车场景的故障模型,将PHAVer模型和故障模型整合,得到包含故障的PHAVer模型,运用PHAVer分析出导致RBC控车场景功能需求不能满足时的功能模块故障情况,实现了对RBC控车场景的安全分析,以便指导后续的系统设计和安全评估。