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

作者：刘金涛; 唐涛; 赵林; 刘玉鹏

来源：中国铁道科学, 2012, (05): 98-104.

• 列车控制系统
• 交接协议
• 混成系统
• UML图
• 微分动态逻辑 Train control system
• Handover protocol
• Hybrid system
• UML diagram
• Differential dynamic logic

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

• 单位
  轨道交通控制与安全国家重点实验室; 北京交通大学