论文部分内容阅读
随着我国高速铁路技术的发展及对高速铁路管理规章制度的出台,我国对CTCS-3(China Train Control System level 3,中国列车运行控制系统)级列控系统的需求规范也逐渐完善。RBC(Radio Block Center,无线闭塞中心)作为CTCS-3级列控系统地面核心子系统用来保障列控系统的安全运营。CTCS-3级列控系统是同时具备了连续和离散的信息交互机制的混成系统,在RBC与其他设备进行交互时如果出现任何与行车许可、线路信息等相关的问题都可能影响高速列车的正常运行,因此需要对RBC控车场景进行安全分析来保证后续的系统安全设计和评估,而基于传统的安全保障技术在列控系统的安全分析中已略显其不足,通过形式化方法对列控系统进行安全分析已经成了研究的主要趋势。本文以CTCS-3级列车运行控制系统中RBC控车场景为研究对象,提出基于UML(Unified Modeling Language,统一建模语言)扩展机制的控车场景功能安全分析方法。首先,针对CTCS-3级列控系统的混成特性,采用面向对象的方法对RBC控车场景进行分析,根据UML扩展机制的安全特性建模方法,构建UML类图和状态转移图模型以及其故障扩展模型来描述系统的状态迁移和连续动态过程,再根据列控系统的需求规范构建具有安全特性的混成概要文件来准确地刻画列控系统的混成特性。然后,选择CPN(Colored Petri Net,有色Petri网)作为UML扩展模型的验证工具及分层控制结构的形式化建模规范,将扩展的UML模型转换成可执行的有色Petri网分层模型,通过ASK-TCL算法对系统模型进行动态行为和状态变化的检验,验证UML扩展模型和RBC控车场景的正确性和一致性。最后,根据已建立的UML扩展模型转化成PHAVer(Polyhedral Hybrid Automaton Verifier,混成自动机模型检验工具)模型,分析RBC控车场景中可能出现的故障并进行描述,将PHAVer和故障模型融合来描述RBC控车场景中设备故障情况以及故障对场景功能产生的影响,利用故障监视器对系统模型进行可达集计算,确定危及系统安全的故障组合实现RBC控车场景的安全分析。结果表明,本文提出的方法可以满足RBC控车场景在需求设计阶段的安全特性要求,为以后列控系统的形式化建模与安全评估提供了参考方法。