| 基于微分动态逻辑的无线闭塞中心交接协议建模与验证 |
| |
| 引用本文： | 刘金涛,唐涛,赵林,刘玉鹏.基于微分动态逻辑的无线闭塞中心交接协议建模与验证[J].中国铁道科学,2012,33(5):98-104. |
| |
| 作者姓名： | 刘金涛 唐涛 赵林 刘玉鹏 |
| |
| 作者单位： | 1. 北京交通大学轨道交通控制与安全国家重点实验室,北京100044;北京交通大学城市轨道交通自动化与控制北京市重点实验室,北京 100044
2. 北京交通大学轨道交通控制与安全国家重点实验室,北京,100044 |
| |
| 基金项目： | 国家"八六三"计划项目，国家自然科学基金委员会与铁道部联合资助项目，国家重点实验室自主课题基金资助项目，北京交通大学-泰雷兹集团国际合作项目 |
| |
| 摘 要： | ETCS-2级列车运行控制系统呈现复杂的混成性。按照无线闭塞中心(RBC)交接协议的内容,建立RBC交接协议的UML图;基于微分动态逻辑理论,从混成系统角度对ETCS-2级列控系统规范中的RBC交接协议进行建模。建立的RBC交接协议模型包括列车子模型、移交子模型和接收子模型。根据模型的性质,构造微分不变式,运用证明工具KeYmaera验证模型的安全性和活性。结合专业知识对关键性的约束条件进行分析并将其反馈至模型,实现模型的精化。在模型验证过程中,发现了交接安全及交接效率的参数约束条件,由此参数约束条件可知,RBC交接效率受RBC离散控制时间和列车运行状况的共同影响。
|
| 关 键 词： | 列车控制系统 交接协议 混成系统 UML图 微分动态逻辑 |
Modeling and Verification of Radio Block Center Handover Protocol Based on Differential Dynamic Logic |
| |
| LIU Jintao
,
TANG Tao
,
ZHAO Lin
,
LIU Yupeng.Modeling and Verification of Radio Block Center Handover Protocol Based on Differential Dynamic Logic[J].China Railway Science,2012,33(5):98-104. |
| |
| Authors: | LIU Jintao TANG Tao ZHAO Lin LIU Yupeng |
| |
| Institution: | 1(1.State Key Laboratory of Rail Traffic Control and Safety,Beijing Jiaotong University,Beijing 100044,China; 2.Beijing Key Laboratory of Urban Rail Transit Automation and Control,Beijing Jiaotong University,Beijing 100044,China) |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
