Modeling Verification And Implementation Research Of Station Data Server For CTCS-1 Train Control System

The C3 high-speed EMU uses general speed line detour operation system(CTCS-1train control system for short)is a new system designed to support the operation of high-speed EMU on general speed line after the fault of high-speed railway line.The system transforms the CTCS-0 train control system widely used on general speed line into CTCS-1 train control system under the premise of minimizing the transformation of the existing equipment on general speed line.It not only solves the safety-related problems existing in general speed line,but also ensures the safe and efficient operation of high-speed EMU on general speed line.Currently,the technical scheme for the system is under study.Station data server(SDS)is the core ground equipment of the system,it sends the generated radio message to onboard equipment through radio broadcast communication.The modeling,verification and realization of SDS can reduce the development cost and risk,and promote the improvement of CTCS-1 train control system scheme.The thesis completes the modeling,verification and realization of SDS based on SCADE.The main work of this thesis is as follows:(1)The software development method based on SCADE is researched,and the overall research scheme of SDS based on SCADE is proposed.The research scheme includes SDS functional requirements analysis,modeling and verification of key scenario for SDS participation,detailed design of SDS functions,modeling,verification and implementation of SDS functions.(2)SDS functional requirements analysis.By sorting out the contents related to SDS in the overall technical specification document of CTCS-1 train control system,the interactive functional requirements and internal functional requirements of SDS are analyzed.The functions of SDS are refined into system self-checking module,data configuration module,dynamic data management module,radio message sending module,status monitoring and recording module.In the process of analyzing the functional requirements of SDS,it was found that the radio one-way broadcasting method was used in the communication between SDS and the train,which has never been used in the existing train control system.Therefore,it is necessary to select radio broadcast communication scenario from the scenarios in which SDS participates for in-depth study.(3)Modeling and verification of radio broadcast communication scenario in which SDS participates.By analyzing the overall technical specification of CTCS-1train control system and the requirements of radio broadcast communication scenario,the radio broadcast communication scenario is designed in detail.The scenario is modeled by Sys ML language,the Sys ML model is transformed into PRISM model through the designed conversion algorithm of Sys ML-PRISM model,and the PRISM model is verified in probabilistic model checking tool PRISM.The rationality of the scenario design and the feasibility of radio one-way broadcast communication are proved,and the technical indicators related to the scenario are confirmed,as the basis of follow-up research.(4)SDS functional modeling verification and implementation.According to the analyzed functional requirements of SDS,the detailed design and SCADE model design of each functional module of SDS are completed.Combined with the scenario-related technical indicators confirmed during the study of radio broadcast communication scenario,the SCADE model of each functional module is improved.The SCADE model of SDS is formed by integrating various functional modules together.The simulation and coverage analysis of the SCADE model of SDS are carried out through the SCADE simulation verification tool to verify the correctness of model and the completeness of simulation.The formal verification method is used to prove that the SDS model can satisfy the safety property,which ensures the safety of SDS.Engineering-oriented C code is automatically generated through the code generator KCG.The C code is put into the target computer for joint test,which verifies that the designed SDS model can meet the expected functional requirements and the feasibility of developing SDS system by SCADE.There are 84 figures,14 tables and 57 references in this thesis.