论文部分内容阅读
无线闭塞中心是我国CTCS-3(Chinese Train Control System at Level3)级列控系统的地面核心子系统之一,是保证列车安全运行的关键设备之一。RBC(Radio Block Center,无线闭塞中心)作为一个复杂且安全苛求的系统,开发时为了更好地保证系统的正确性,需要一套全面有效的建模与验证方法。本文以RBC系统的切换功能为对象进行建模研究。通过阐述CTCS-3级列控系统中RBC的工作原理,明确了RBC系统的安全需求和功能需求。对UML(Unified Modeling Language)和有色Petri网(CPN,Colored Petri Nets)各自的优缺点进行对比分析后,发现二者特性存在互补性,可以将这两种建模方法结合应用,据此设计出基于UML和有色Petri网的RBC系统建模方案,并对UML转换为有色Petri网的基本规则进行研究。为了验证上述集成建模方法的有效性,选取RBC系统的切换功能,对其功能需求以及切换策略深入分析,重点对该集成建模方法在双电台切换策略下的应用进行研究。首先设计双电台切换过程的切换流程,然后选用UML的用例图、顺序图和状态图对切换需求进行描述,再根据UML到有色Petri网的转换规则建立对应的有色Petri网模型,最后引入分层结构建立层次化的RBC切换CPN模型。利用CPN Tools建模工具对所建立的模型进行功能验证,生成相应的状态空间报告和可达图,状态空间报告中对模型的有界限、活性、家态性以及公平性等动态属性作出详细说明,可达图主要是对模型的逻辑正确性进行验证,并运用状态问询命令验证模型的功能是否与设计初衷相符。验证结果表明建立的模型能够反映RBC切换过程的功能特性。在验证了模型功能完备的基础上,给模型添加时间因素,得到RBC切换的赋时模型,利用CPN Tools建模工具中的监控器机制,采集该模型仿真数据,通过整理多次仿真的数据,得到RBC切换赋时模型在不同的通信质量下的时间性能分析,其分析结果为完善RBC系统研发提供依据。