Modeling And Verification Of Operation Scenarios Of Train Control System For Train-to-Train Communication Based On CPN

With the rapid development of train control technology,urban rail transit will continue to innovate and optimize,and develop vigorously in the direction of high efficiency,intelligence,and safety.Train Control System for Train-to-Train Communication has become the development direction of the next generation of train control system.As a new intelligent train control system,Train Autonomous Circumambulate System focuses on train selfdiscipline,and the system can monitor data interaction between two trains in real time,thereby achieving resource management and autonomous control between trains.Unlike CBTC,TACS has not been put into operation for a long time,and the system architecture and function division have also changed.Therefore,formal modeling and logical Functional verification are required for the typical operation scenarios of the system under the new functions.For the operation scenarios of train control systems under complex interactions,traditional security analysis methods may face certain challenges.STPA method categorizes the main factor causing danger as abnormal interactions between components,meeting the requirements of TACS system operation scenarios for security analysis methods.In view of the new functions of TACS based on Train-to-Train communication,such as autonomous resource management and active interval protection,this thesis selects typical operation scenarios and uses Colored Petri Net theory as the modeling basis.From the perspective of formal methods,The formal modeling and simulation verification of TACS operation scenarios are carried out.Taking the generation scenario of movement authority for train operation in the train section as the research object of safety analysis,TACS system scenario safety analysis method based on STPA method is proposed to identify unsafe control behaviors and potential dangers,and obtain formal safety requirements.The research work is as follows:(1)Based on the research status of Train Control System for Train-to-Train Communication at home and abroad,the architecture of CBTC and TACS was compared and analyzed,and the equipment composition and system functions of TACS were described.In view of the process that changes the system function allocation,the typical operation scenarios of TACS are selected after comparing the results,such as the generation scenario of movement authorization in train interval,the scenario of train reentry and the scenario of train fault degradation.The information interaction between devices in each scenario is analyzed in detail to lay the foundation for subsequent modeling.(2)Based on the CPN theory,construct CPN models for the above three operational scenarios based on the “top-down” model reigorization strategy.The state spatial analysis of CPN-Tools is used to verify the basic attributes and correctness of the model,which proves the effectiveness of the modeling method.On the basis of successful model logic Functional verification,the simulation performance analysis of the model is carried out.The results show that the end-to-end communication transmission delay in the process of movement authority generation meets the requirements of Long Term Evolution for Metro to carry the quality of service of CBTC services;Due to the refinement of turnout resources in the turn back process after the train station,the turn back time of TACS is shorter than that of traditional train control system,further improving the line transportation capacity.The model established in the process of train failure degradation can realize the function of train fault degradation under the condition of abnormal communication failure,which verifies the correctness and integrity of the functional design.(3)On the basis of formal modeling,using STPA method for security analysis of operational scenarios.Select the movement authority generation scenario for train operation within the interval,define system level accidents and system level hazards,establish corresponding STAMP models,obtain detailed unsafe control behaviors,detailed safety constraints,safety requirements,convert safety requirements into temporal logic expressions,and perform formal verification to provide support for technical personnel in subsequent system optimization.