Modeling And Verification Of Complex Scenarios Of Autonomous Chinese Train Control System Level 3

High-speed railways in China has achieved a rapid development in recent years,the train control system integrates with other advanced technologies continuously,such as communications technologies,networking technologies,and computer technologies.The increasing improvement in automatic extent and the expansion of system hardware and software has led to the increasing complexity in the train control system.As a complex safety-critical system,it is an important research topic to work on how to guarantee the correctness of train control system.Compared with the domestic CTCS-3 train operation control system,the hardware and software of the autonomous CTCS-3 train operation control system are all researched and developed independently.It has independent property right with the new functional requirements,which means that it needs more comprehensive analysis on the system according to the regulations.In order to ensure the safety of the system and the cross line operation capability of CTCS-3,this paper starts with the real-time performance of the train control system to study on the modeling and testing of the operational scenarios,and has mainly completed the following works:(1)Select timed automata theory to verify the real-time performance of the system through the comparison with several formal methods of system verification,and introduce the timed automata theory and the use method of its model testing tool UPPAAL.(2)Take the code sequence testing scenarios and the complex scenarios as examples to analyze the work flow of the system equipment in different situations.Use time automata theory to establish the work flows of code testing scenarios,and the timed automaton models of work flows in the complex scenarios after reasonable ion and hypothesis according to the characteristics of the research objects.(3)Analyze and verify the testing tools of UPPAAL application in the above two scenarios:construct the product of timed automaton by setting channels and overall variables;use the simulator to simulate the interaction of equipment in different scenarios and analyze the status changes of running trains;use the validator to test the safety,immediacy and activation of the system,and prove the validity of the modeling testing method.(4)On the basis of participating in the high-speed comprehensive experiment of Datong-Xi'an high-speed railway,this paper Analyze and extract the flow of information interaction in the system equipment operational scenarios of different manufactures' autonomous CTCS-3 system,and write test sequences based on the actual operational data.Meanwhile,with the inter-connected test platform of CTCS-3 in the laboratory,the platform software is modified to be better used in the CTCS-3 and conduct simulation test.