|
|||||
|
|
| CTCS-3级列控系统RBC控车场景建模与验证 | |
| 作者单位： | ;1.兰州交通大学自动化与电气工程学院 |
| 摘 要： | 应用统一建模语言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 |
Modeling and Verification of Train Controlling of RBC Scenes on CTCS-3 System |
|
| Institution: | ,School of Automation & Electrical Engineering,Lanzhou University |
| Abstract: | |
| Keywords: | CTCS-3 system Train controlling of RBC scenes UML PHAVer |
| 本文献已被 CNKI 等数据库收录！ | |