| The new generation CTCS-1(Chinese Train Control System-Level 1)train control system is a technical upgrade of the existing railway train control system,which aims to enhance the safety,reliability,transportation efficiency and automation of general-speed trains.It meets current requirement of putting on-board railway data down to the ground,realizing trackside train control center’s unified management of line data,guaranteeing immediate update of temporary speed restriction,reducing driver’s operation on train control data and improving the automation level of train control equipment in existing railway.Regional Data Center(RDC)is the core trackside equipment of CTCS-1 train control system,it is responsible for the management of CTCS-1 trains and provides CTCS-1 train movement data through wireless network,which includes line data,link balises,route data and temporary speed restriction information.The formal modeling and verification analysis of RDC can ensure the completeness,security and reliability of RDC system software and promote the technical upgrading of the existing railway train control equipment.The thesis chose Timed Colored Petri Nets(TCPN)based on ML language to carry out functional design,modeling,simulation and verification analysis research of RDC system.The main work completed in this thesis is as follows:Firstly,TCPN formal modeling and analysis method for real-time concurrent systems was proposed based on the characteristics of Colored Petri Nets and Timed Petri Nets,and the general process of modeling and analysis for TCPN method based on ML language was summarized,on this basis,constructing the overall framework of CTCS-1 RDC modeling and verification analysis,and the framework covered RDC requirements analysis,functional design,modeling,functional verification analysis,software architecture design,software development,simulation realization and so on.Then,RDC overall functional design and main module functional design were carried out after analyzing the characteristics of RDC system,its internal functional requirements and interactive functional requirements.And module functional design covered the main operation scenarios such as CTCS-1 train startup,registration,logout,train control level conversion,movement data generation and train handover.The functional differences contrastive analyses were also implemented between RDC and CTCS-3 RBC in main operation scenarios.Secondly,RDC interactive functional TCPN model and main functional TCPN model were established respectively according to the designed RDC function;and hierarchical idea of Timed Colored Petri Nets was used to reduce the model complexity and state space dimension.The main function model was subdivided into on-board equipment self-check submodel,RDC work status inspection submodel,RDC and C1-ATP link establishment submodel,communication session establishment submodel,train data confirmation submodel and operation data interaction submodel.At the same time,establishing extraordinary scene models,such as train control level conversion model,train handover model,C1 train and general-speed train tracking operation model,and then the simulation model was verified and analyzed through simulation verification tool CPN-Tools from the perspective of functional logic correctness,completeness and consistency of technical specifications.Besides,taking train handover scene as an example to analysis RDC time performance on the basis of the successful verification of its logic functions.Finally,RDC system software hierarchical architecture was designed and software was developed according to RDC functional model,and RDC simulation software was tested on the laboratory platform of train control system.Through the "five stations and four sections" application scenario test,the correctness of RDC formal functional model and the feasibility of software development for RDC system were verified. |
PDF Full Text Request