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

Modeling and Verification of Radio Block Center Handover Protocol Based on Differential Dynamic Logic

作　　者：刘金涛[1,2] 唐涛[1,2] 赵林[1,2] 刘玉鹏 

机构地区：[1]北京交通大学轨道交通控制与安全国家重点实验室,北京100044 [2]北京交通大学城市轨道交通自动化与控制北京市重点实验室,北京100044

出　　处：《中国铁道科学》2012年第5期98-104,共7页China Railway Science

基　　金：国家"八六三"计划项目(2011AA010104);国家自然科学基金委员会与铁道部联合资助项目(60634010;60736047);国家重点实验室自主课题基金资助项目(RCS2008ZQ002;RCS2008ZZ005);北京交通大学-泰雷兹集团国际合作项目(M&V-SCHS)

摘　　要：ETCS-2级列车运行控制系统呈现复杂的混成性。按照无线闭塞中心(RBC)交接协议的内容,建立RBC交接协议的UML图;基于微分动态逻辑理论,从混成系统角度对ETCS-2级列控系统规范中的RBC交接协议进行建模。建立的RBC交接协议模型包括列车子模型、移交子模型和接收子模型。根据模型的性质,构造微分不变式,运用证明工具KeYmaera验证模型的安全性和活性。结合专业知识对关键性的约束条件进行分析并将其反馈至模型,实现模型的精化。在模型验证过程中,发现了交接安全及交接效率的参数约束条件,由此参数约束条件可知,RBC交接效率受RBC离散控制时间和列车运行状况的共同影响。ETCS-2 presents the characteristics of complex hybrid. According to the handover protocol of Radio Block Center (RBC), the UML diagram of RBC handover protocol is given. Modeling is carried through on the RBC handover protocol in ETCS-2 train control system specification from the point of hybrid system based on differential dynamic logic. The established model of RBC handover protocol consists of train submodel, handover submodel and takeover submodel. According to model characteristics, differential invariants are structured and proved by KeYmaera to validate the safety and liveness of the model. Combining with the domain knowledge, the key constraints are analyzed and fed back to the initial model in order to refine the model. During model validation process, the constraints for handover safety and efficiency parameters are found. It's known from parameter constraints that RBC handover efficiency is influenced by both the discrete control time of RBC and the running state of the train.

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

分 类 号：U284.482[交通运输工程—交通信息工程及控制]