摘要：应用统一建模语言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级列控系统需求规范的正确性。

关键词：rbc控车场景 uml phaver 

单位：兰州交通大学自动化与电气工程学院; 兰州730070