Modeling And Verification Of Tracking Operation Module In Train-ground Collaborative Control System

The train control system is the key technical equipment to control the speed of the train and ensure the safety and efficiency of the train operation.The traditional train control system takes ground central equipment as the main part.Under this framework,train operation-related data is transmitted to the ground control center for processing,and then the processing results are returned to the train.There exist problems of excessive lineside equipment,complex structure and low autonomy degree of train.With the development of train autonomous positioning,communication and control technology,research on the next generation train control system is in progress.In response to the needs of the intercity railway train control system to reduce lineside equipment,improve train autonomy and intelligence and improve transportation capacity,train-ground collaborative control system was proposed.The system transfers part of the functions of the ground equipment to the vehicle equipment.The train operation control function is completed by the cooperative work of vehicle and ground equipment,thereby the system structure is simplified,the function allocation is optimized,and the autonomy degree of train is improved.As a new train control system,strict analysis and verification are required before it is put into use,so as to discover possible design defects in the system in time and ensure that the system meets the safety and functional requirements.This thesis takes the tracking operation module that completes the train operation function in the train-ground collaborative control system as the research object.The specific function realization is designed and verified by formal methods.The main work of the thesis is as follows:(1)The function realization of the tracking operation module is analyzed and designed in the train-ground collaborative control system.According to the structure and technical characteristics of the train-ground collaborative control system,the information interaction between each functional sub-module is clarified.For the Movement Authority generation and security protection functions in the tracking operation module,the functional requirements are analyzed,the sources of information are clarified,and the specific implementation processes are designed.The Movement Authority function is divided into safe position calculation,train route inquiry and Movement Authority calculation in different scenarios;the safety protection function is divided into the issuance of temporary speed restriction command,monitoring curve generation and real-time speed monitoring.(2)The formally models of tracking operation module are established by hierarchical colored Petri nets.The top-level model is established based on the functional requirements of the tracking operation module to describe the overall functional requirements.Based on the system architecture and functional division,hierarchical models are established for the specific implementation processes of Movement Authority calculation and security protection sub-modules,so as to reduce the complexity of the model.The models describe the internal information interaction and state changes in the processes of sub-modules’ function implementation respectively.(3)Movement Authority generation and security protection functions are formal verified of the tracking operation module in train-ground collaborative control system.The initial identifications of the models are set based on specific data.Dynamic simulations are conducted by modeling tools to observe the behavior and state changes of the models,and the correctness of the models is verified and analyzed through the model state space reports and nodes information.The verification results show that the model can effectively complete the system functions,and the correctness of the models attributes meets the requirements,which provides a theoretical reference for the system development work in the design stage.