| ABSTRACT:In order to meet the requirements of high speed and high capacity in railway transportation, train control system which makes the train not to exceed the speed and distance limits, is very essential to ensure the traffic safety and improves the operation efficiency. As radio communication with real-time, bi-directional, large-capacity and other advantages, CTCS level-3adopts the GSM-R to transfer information between the wayside and onboard equipment to achieve train control based on communication.The reliability of wireless communication is lower compared to wired communication, the communication failures in train control system may cause accidents and have impact on operational efficiency, so it is very necessary to model and analyze the wayside-to-train communication system of CTCS level-3. This provides a theoretical basis for solving practical problems of railway signalling safety communication, and it helps to avoid or reduce the occurrence of accidents and improve operational efficiency in railway signaling.In this paper, after an in-depth understanding the structure and function of wayside-to-train communication system of CTCS level-3, the method of combination of simulation and model checking is proposed to model and analyze the system for its distribution, probabilistic, real-time characteristics. Simulation method can simulate the behavior of the system better, formal methods can analyze the performance of the system rigorously, and this approach combines the advantages of simulation and formal methods. The main work of this thesis is as follows:(1)The hierarchical model and communication process of wayside-to-train communication system of CTCS level-3are described, the impact of communication performance on traffic safety and operational efficiency is also analyzed.(2) Modeling and analysis methods of communications system are reviewed, the basic principles of discrete event simulation and probabilistic model checking are also introduced.(3) The matlab SimEvents is used to model the wayside-to-train communication system, then the information exchange process is acquired by simulation, and the statistical of safe connection setup and wireless message transmission time delay is analyzed based on the simulation results. (4) Because simulation cannot verify the system performance rigorously, the probabilistic model checking methods is adopted to model the wayside-to-train communication system, the probability distributions of safe connection setup and wireless message transmission time delay is analyzed based on probabilistic model checking tool PRISM, and the method is compared with SimEvents methods.(5) On the basis of wayside-to-train communication system, SimEvents and PRISM are adopted to analyze the response time of train control system. The probability distributions of response time from sending postion report to reception of movement authority are analyzed. It shows that this method has good scalability and application value.Modeling and analysis CTCS level3wayside-to-train communication system based on SimEvents and PRISM realize simulation and formal verification. The method of wayside-to-train communication system and its result can be applied to train control system performance analysis. |