Research And Verification Of Moving Block Function Of VBTC System Based On Timed Automata

With the development of the Communication Based Train Control(CBTC)signal system of urban rail transit and the application of 5th Generation Mobile Networks(5G)technology,the research of train operation control system based on Vehicle-to-vehicle Communication(VBTC)came into being.The system breaks through the traditional CBTC system train control mode with ground equipment as the core,reorganizes the system architecture,optimizes the system functions,realizes the moving block function with on-board equipment as the core,improves the flexibility and intelligence of the train,at the same time,due to the simplification of ground equipment,the interface between the systems is simplified,the control information reaches the train directly,and reduces the system response time.As the key function of VBTC system,the correctness and effectiveness of moving block must be guaranteed.Formal verification and simulation test verification can verify the formulation of Intelligent Vehicle On-board Controller(IVOC)system specifications and the realization of system functions,discover the possible unsafe factors in the process of system development in time,which has theoretical value and practical significance for the research and application of the system.Based on the architecture of VBTC system,this thesis focuses on the three main functions of moving block function: front train identification,train sieving and on-board Movement Authority(MA)generation.The realization of the above functions is formally described and verified by using Timed Automata(TA)theory and UPPAAL tools,and the test verification is completed on the test platform,which verifies the rationality and effectiveness of system function development.The specific work is as follows:(1)Based on the analysis of the functions and characteristics of VBTC system,this thesis focuses on the analysis of the functions of the on-board moving block of the IVOC subsystem.The functional requirements of the main modules to realize the function of moving block is analyzed,and the specific functions and processing flow of the system modules in the process of front train identification,train sieving and MA generation process are analyzed,and the information interaction between the subsystem modules in the process of realizing the function of each module are analyzed,which lays the foundation for the system modeling and verification.(2)According to the Verification,Validation and Accreditation(VV&A)theory of train control system and the modeling process of TA,combined with the process of front train identification,train sieving,MA generation and the information interaction between system modules,the TA network models are established respectively.The Backus-Naur Form(BNF)verification syntax based on UPPAAL was used to describe the security and restricted activityof each module,and the related verification was completed.(3)The simulation test platform of VBTC system was built,and the test cases of train identification,train sieving and MA generation module were designed.According to the test case and the test execution process,the system function test is completed.