摘要
应用统一建模语言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级列控系统需求规范的正确性。
Complex compositeness of train controlling of RBC scenes on CTCS-3 system containing RBC logout, RBC registration start, level transfer and movement authority is studied with UML and PHAVer. Firstly, UML extensibility mechanism of the stereotype is used to extend UML, establish UML model of train controlling of RBC and implement complex compositeness of train controlling of RBC scenes description. Then, UML model of train controlling of RBC is transformed into PHAVer model based on transformational rules between UML and PHAVer. Finally, functional requirements for train controlling of RBC scenes are summarized according to CTCS-3 system functional requirement specification, and the correctness of CTCS-3 system functional requirement specification is verified.
作者
盛昭君
米根锁
SHENG Zhao-jun MI Gen-suo(School of Automation ＆ Electrical Engineering, Lanzhou University, Lanzhou 730070, Chin)
出处
《铁道标准设计》
北大核心
2017年第11期143-147,共5页
Railway Standard Design
基金
甘肃省自然科学基金项目(1310RJZA046)
