CTCS-3级列控系统RBC控车场景建模与验证

摘要：

应用统一建模语言UML与模型检验工具PHAVer(Polyhedral Hybrid Automaton verifier)相结合的方法,研究CTCS-3级列控系统RBC控车场景:列车注册与启动、行车许可、等级转换、列车注销的混成性.首先通过UML支持的扩展机制,引入构造型(Stereotype)对UML进行面向混成性的扩展,建立RBC控车场景UML模型,实现对RBC控车场景混成性的描述.然后依据UML到PHAVer的转换规则,将UML模型转换成PHAVer模型.最后,依据CTCS-3级列控系统需求规范,总结RBC控车场景的功能需求,运用PHAVer进行验证,证明CTCS-3级列控系统需求规范的正确性.

关键词：CTCS-3级系统、RBC控车场景、UML、PHAVer

所属期刊栏目：61

分类号：U238.2(特种铁路)

资助基金：甘肃省自然科学基金项目1310RJZA046

在线出版日期：2017-12-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：143-147