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

摘要：

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

关键词：列车控制系统、交接协议、混成系统、UML图、微分动态逻辑

所属期刊栏目：33

分类号：U284.482(铁路通信、信号)

资助基金：国家高技术研究发展计划（863计划）;国家自然科学基金;国家重点实验室自主课题;国家国际科技合作专项基金

在线出版日期：2012-12-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：98-104