Simulation And Verification Of Intercity Railway Train Control System Operational Scenario Based On Model

With the development of train control technologies,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.On the one hand,Simulink and Stateflow can support graphical modeling and simulation and can eliminate some security risks in the phase of system design and development.On the other hand,Formal methods based on rigorous mathematics definition have become an important modeling and verification theory in the field of train control systems due to its accurate and clear description of system architecture.So applying formal verification technology on the simulation model provides a new idea to solve the modeling and verification problem of train control system.Starting from the hybrid properties of intercity railway train control system,this paper studied the simulation and verification of the operational scenario.A method integrated with modeling,simulation and verification is proposed to guarantee the correctness of intercity railway train control system.The main works of this thesis are summarized as follows:Firstly,in view of the hybrid properties of intercity railway train control system,this paper studies a method about modeling and simulation of train control system based on Simulink/Stateflow.A hierarchical model of intercity railway train control system is established;the typical activities and information interaction of each equipment in the train control system is described by scenario technology;the process of modeling and simulation is also given in this paper.Secondly,based on the theory of hybrid automata,a method is researched to ensure the correctness of intercity railway train control system by applying formal verification technology on simulation model.By analyzing the formal semantics of the Simulink/Stateflow model and the hybrid automata model,the conversion rules of the Simulink/Stateflow model and the hybrid automata model are given to ensure the model consistency,and the verification process of scenario model based on SpaceEx platform is given.Thirdly,based on MATLAB environment,the simulation platform of scenario of automatic train operation in intercity railway train control system is built.This platform uses the real data as the underlying driver.The emergency braking distance produced by the model is compared with the real data in the experiment.The operation of train under different parameter combinations is simulated and analyzed,Simulation results under a certain case reproduce a security problem found in the test site.Finally,this paper takes a typical case of operational scenario which is automatic train operation scenario as a verification case.The proposed model transformation rules are used to convert the simulation model of the scenario into a hybrid automaton model.The modeling,verification and analysis of the operational scenario are completed in the SpaceEx tool,which proves the feasibility of modeling and verification method for intercity railway train control system.