科研之友
微信
新浪微博
Facebook
分享链接
摘要
区域控制器(zone controller, ZC)是一个实时复杂系统,它要求过程控制的准确性。列车追踪场景是城市轨道交通(communication based train control, CBTC)系统中ZC的一个重要功能。在对系统进行深层次的开发设计过程中需要对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性。通过分析ZC系统结构及列车追踪分界点处理过程,给出满足系统安全性的功能要求和性能要求,并采用统一建模语言(unified modeling language, UML)与时间自动机相结合的方式建立列车追踪场景中列车筛选和列车追踪分界点的时间自动机网络模型。同时,应用UPPAAL验证工具对系统进行仿真模拟,验证了系统的功能和性能要求。结果表明,列车追踪分界点功能满足系统安全性和受限活性的规范要求。因此,此种建模方法是可行的,可以将其应用于列控系统其他场景的建模与验证过程中。
-
单位兰州交通大学; 机电工程学院
