Formal Modeling And Analysis For Generation Of Train Movement Authority In RBC Of CTCS-3

CTCS-3train control system is suited to Chinese characteristics, which is developed in the case of introducing, absorbing and innovating the new foreign technologies. At present, CTCS-3is vigorously researched and applied in domestic, and it greatly improves the reliability and safety of railway transportation. However, the train control system still requires improvements and studies according to the basic national conditions of Chinese railway. And requirements specification is the starting point and basis for system development, so it is necessary to strictly analyze and validate specification of the train control system, and eliminating the normative ambiguity to make the train control system safer and more reliable.Movement authority (MA) management is one of the main functions of RBC. According to the different operation scenes of train, RBC calculates different MA and sends it to the train in order to ensuring the safety of the train. So it is of great significance to safe and efficient operation of the train control system that analysis of the generation process of the MA in accordance with requirement specification.To solve the problems, firstly, this paper designed different modules in application layer based on the different functions of MA; secondly, this paper researched different generation processes of the MA under different operation scenes of the train; finally, according to the generation of MA principle of RBC in the CTCS-3, this paper proposed a model of MA based on the colored Petri net, by CPN-Tools simulation tool for dynamic simulation to analyze the generation process of MA under different operation scenes of the CTCS-3control system, observing the communication mechanism and message transmission during the operation of train. And this paper analyzed some properties and influence of time on the generation process of MA by using the state space analysis and performance analysis.Simulation results show that the established model meets the design requirements, and it can complete the MA calculation under the different operations of the scene. The state space report graphs verify that some properties of the system conform to the specifications of train control systems. Finally the joined parameters optimize the design model, getting the most reasonable delay range of the system. This paper provides a normative and correct software design method for the design of MA model. It reduces some flaw in the software development process, and makes the train operation safer and more reliable.