Modeling And Verification Of Regional Data Center For CTCS-1 Train Control System Based On SysML And Timed Automata

With the upgrade and development of railway system,the improvement of safety and efficiency for the existing railway lines has been put on the agenda.The Chinese Train Control System level 1(CTCS-1)is a new system designed for the existing railway lines,aiming to enhance the safety,reliability,efficiency and automation of the trains with speed below 200km/h.It has obvious advantages over the existing railway system,which can solve many problems at a lower cost.Regional Data Center(RDC),as the key trackside equipment of CTCS-1,can send real-time data to trains through radio transmission,which greatly reduces the on-board data storage,and at the same time,reduces the driver operation and the hidden dangers of human factors.This thesis completes the establishment and verification of the RDC function models,including the information interaction between RDC and external systems and the generation of movement data,which can lay the foundation for the practical application of the CTCS-1.The main works of this thesis is as follows.Firstly,the functional requirements of CTCS-1 and RDC,including the internal functions and external interaction functions are studied.Then,its characteristics are summarized to conduct the requirements modelling.Based on the previous research on modelling of train control system,the SysML modeling language and the time automata theory are adopted to conduct the modelling and verification of RDC.Secondly,by analyzing the information interaction process of RDC external interaction module,the RDC interaction process is divided into two parts:the ground equipment interaction module and the onboard equipment interaction module.RDC interaction process includes equipment startup,train registration,normal operation,train deregistration,and RDC handover.The SysML sequence diagram is used to model the above scenarios,and is transformed into timed automata network models,and then validated in UPPAAL.Thirdly,the generation of movement data in RDC is studied.RDC obtains information from external interaction modules,including temporary speed restriction(TSR)provided by Temporary Speed Restriction Server(TSRS),train route information provided by Computer based Interlocking(CBI),train position information provided by onboard equipment,and generates dynamic path data according to different operation scenarios,including the creation of train path and the extension of TSR.Combined with the static path data stored in RDC,it generates train movement data and sends it to the onboard equipment through wireless network to control train operation.The SysML activity diagram is used to model the above processes,and the model of RDC movement data generation is obtained,which is transformed into a timed automata network model and verified in UPPAAL.Finally,based on the modeling analysis,the design and development of RDC simulation software is completed.The correctness and rationality of the RDC function model is verified by the system debugging test on a laboratory platform based on the real scenario of a certain section of Beijing-Shanghai line.