基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证

• 作者: 吕继东 唐涛 徐天华 燕飞
• 来源期刊: 铁道学报
• 学科: 交通运输
• 关键词: 区域控制子系统 UPPAAL 时间自动机 自动验证
• 年，卷（期）: 2009,（3）
• 页码范围: 59-64
• 页数: 6页
• 分类号: TP393|U283
• 字数: 3404字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-8360.2009.03.011

摘要

CBTC(Communication Based Train Control)系统可有效提高轨道交通的列车运营效率,降低系统建设和维护费用.在系统研发过程中需对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性.CBTC区域控制子系统是一实时控制系统,它要求控制时间的精确性和控制过程的准确性.本文通过分析城市轨道交通CBTC区域控制子系统的结构,给出满足该子系统安全性的功能和性能要求,并结合时间自动机理论方法提出包含列车、速度距离控制器、区域控制器和多车控制队列的时间自动机网络模型.同时,应用UPPAAL验证工具对CBTC区域控制子系统进行仿真建模,并验证该子系统功能和性能要求,从而保证了系统模型的安全性和受限活性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
2	吕继东	北京交通大学轨道交通控制与安全国家重点实验室	25	310	9.0	17.0
3	燕飞	北京交通大学轨道交通控制与安全国家重点实验室	25	548	12.0	23.0
4	徐天华	北京交通大学轨道交通控制与安全国家重点实验室	1	52	1.0	1.0