基于微分动态逻辑的无线闭塞中心交接协议建模与验证

• 作者: 刘玉鹏 刘金涛 唐涛 赵林
• 来源期刊: 中国铁道科学
• 学科: 交通运输
• 关键词: 列车控制系统 交接协议 混成系统 UML图 微分动态逻辑
• 年，卷（期）: 2012,（5）
• 页码范围: 98-104
• 分类号: U284.482
• 字数: 5865字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-4632.2012.05.15

摘要

ETCS-2级列车运行控制系统呈现复杂的混成性.按照无线闭塞中心(RBC)交接协议的内容,建立RBC交接协议的UML图；基于微分动态逻辑理论,从混成系统角度对ETCS-2级列控系统规范中的RBC交接协议进行建模.建立的RBC交接协议模型包括列车子模型、移交子模型和接收子模型.根据模型的性质,构造微分不变式,运用证明工具KeYmaera验证模型的安全性和活性.结合专业知识对关键性的约束条件进行分析并将其反馈至模型,实现模型的精化.在模型验证过程中,发现了交接安全及交接效率的参数约束条件,由此参数约束条件可知,RBC交接效率受RBC离散控制时间和列车运行状况的共同影响.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
5	赵林	北京交通大学轨道交通控制与安全国家重点实验室	11	160	8.0	11.0
9	刘金涛	北京交通大学轨道交通控制与安全国家重点实验室	7	110	6.0	7.0