车车通信系统中车地控制机理分析及验证

车车通信系统是一种以列车为中心的控制系统,取消了轨旁联锁系统,列车直接与地面对象控制器通信进而控制道岔。这种车地直接控制方式提高了系统效率的同时,也成为系统的关键安全因素。为了实现车车通信系统中的车地设备安全控制,提出唯一秘钥实现控制流程,为了验证其安全性,使用基于标签转移系统的形式化方法进行验证。基于车车通信系统的控制机理和车地控制场景,建立唯一秘钥的车地控制流程的形式化模型,并LTSA软件对模型进行安全检测,最后通过实例验证了车地控制流程的可行性和有效性。

Analysis and Verification of Control Mechanism between Train and Wayside Equipment in VBTC System

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 is proposed to fulfill control process, the formal verification method by the label transfer system (LTS) is 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 is established by the formal language, the LTSA software is used to carry out safety inspection of the model, and finally the feasibility and validity of the vehicle control process by example is verified.