Modeling And Verification Of CBTC System Security Communication Protocol Based On Time Automaton

According to the newly published "China urban rail transit operation and development report(2019-2020)" in 2020,China’s urban rail transit is developing rapidly,and its total operating mileage has exceeded 6700 km.However,due to the early planning,development and construction and other objective reasons,China’s urban rail transit operation organization is still single line independent operation,and the line capacity is greatly limited.When it is impossible to speed up the evacuation of passengers at the transfer station by increasing the train service frequency,the network operation mode of interconnection becomes an important means to reduce the number of passenger transfer and relieve the pressure of station transfer.To sum up,the realization of interconnection between urban rail transit lines is a main goal of railway signal research.Communication based train control(CBTC)system is the mainstream signal system of urban rail transit in China.At present,RSSP-Ⅱ security communication protocol is mainly used in CBTC system.At present,there is little research on the test of railway communication protocol.There is no unified standard for Metro Signal Equipment in China.Each manufacturer has different understanding and implementation methods for the safety communication between systems,which leads to the failure of interconnection between CBTC systems and affects the operation efficiency,Therefore,it is very important to carry out the research on secure communication protocol and establish the relevant CBTC system simulation test platform.This thesis mainly completed the following research content:This thesis first establishes RSSP-Ⅱ railway safety communication protocol as the research object for analysis,focuses on the analysis of the security function module designed for the open transmission system structure in the protocol,and analyzes the function of the security application middle sub layer and the message authentication security layer in the security function module,After the analysis,we extract the security layer connection establishment and release process and timestamp initialization process as the main research objects.Secondly,the formal method is selected as the tool of communication protocol research,and the formal modeling method is used to analyze the protocol.In this thesis,a modeling method based on timed automata theory is used to analyze the formal modeling of the whole layer connection establishment and release process and timestamp initialization process.The model is simulated and verified by the model tool UPPAAL,which verifies the security and time efficiency of the design.Finally,with the help of CBTC simulation platform of the laboratory,the test subsystem is developed and designed,the specific test process of the system is established,and the test case of CBTC system is designed according to the established formal model.Aiming at the communication test work in this thesis,the communication test module of simulation subsystem is designed to complete the communication detection function and communication test function in the module,and the corresponding communication fault injection function is designed to complete the corresponding communication test work.