中国铁道科学2012，Vol.33Issue(5)：98-104,7.DOI:10.3969/j.issn.1001-4632.2012.05.15
基于微分动态逻辑的无线闭塞中心交接协议建模与验证
Modeling and Verification of Radio Block Center Handover Protocol Based on Differential Dynamic Logic
摘要
Abstract
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图/微分动态逻辑Key words
Train control system/ Handover protocol/ Hybrid system/ UML diagram/ Differential dynamic logic分类
交通工程引用本文复制引用
刘金涛,唐涛,赵林,刘玉鹏..基于微分动态逻辑的无线闭塞中心交接协议建模与验证[J].中国铁道科学,2012,33(5):98-104,7.基金项目
国家"八六三"计划项目(2011AA010104) （2011AA010104）
国家自然科学基金委员会与铁道部联合资助项目(60634010,60736047) （60634010,60736047）
国家重点实验室自主课题基金资助项目(RCS2008ZQ002,RCS2008ZZ005) （RCS2008ZQ002,RCS2008ZZ005）
北京交通大学-泰雷兹集团国际合作项目(M&V-SCHS) （M&V-SCHS）
