摘要
车车通信系统是一种以列车为中心的控制系统,取消了轨旁联锁系统,列车直接与地面对象控制器通信进而控制道岔。这种车地直接控制方式提高了系统效率的同时,也成为系统的关键安全因素。为了实现车车通信系统中的车地设备安全控制,提出唯一秘钥实现控制流程,为了验证其安全性,使用基于标签转移系统的形式化方法进行验证。基于车车通信系统的控制机理和车地控制场景,建立唯一秘钥的车地控制流程的形式化模型,并LTSA软件对模型进行安全检测,最后通过实例验证了车地控制流程的可行性和有效性。
The vehicle based train control(VBTC)system is a kind of train centric control system,the interlocking system in the wayside is removed,and the train communicates directly with the ground object controller to control the point machine.This kind of direct communication mode improves the system efficiency,and it also becomes the key safety factor in the system.In order to realize the safe vehicle-to-wayside control in the VBTC system,the only key implementation was proposed to fulfill control process,the formal verification method by the label transfer system(LTS)was used to verify its safety.Based on the control mechanism in the VBTC system and vehicle-to-wayside control scene,the formal model of vehicle-to-wayside control process based on the only key implementation to was established by the formal language,the LTSA software was used to carry out safety inspection of the model,and finally the feasibility and validity of the vehicle control process by example was verified.
作者
冯浩楠
FENG Hao-nan(Signal and Communication Research Institute,China Academy of Railway Sciences Corporation Limited,Beijing 100081,China;The Center of National Railway Intelligent Transportation System Engineering and Technology,Beijing 100081,China)
出处
《科学技术与工程》
北大核心
2020年第13期5345-5349,共5页
Science Technology and Engineering
基金
中国铁道科学研究院通信信号研究所重点计划(1852TH0503,1851TH6602)。
关键词
车车通信系统
车载联锁系统
对象控制器
车地控制
道岔
形式化验证
标签转移系统
vehicle based train control system
on board interlocking system
object controller
vehicle to wayside control
point machine
formal verification
label transition system
