Railway marshalling yard operation is developing towards high density, fast turnover and fine scheduling, which puts forward higher requirements for reliability verification of hump disassembly plan. The operation plan of a railyard involves discrete events such as train arrival, locomotive occupancy, hump authorization, carriage roll-off and fault recovery. Traditional empirical verification is difficult to accurately describe the completion probability under random disturbances. In this paper, statistical model checking method is used to analyze the reliability of railway marshalling yard operation plan. In this paper, the main controller, train, shunting locomotive and hump signal system are abstract as timed automata with stochastic time semantics. The synchronization channel is used to describe the events of unwinding start, roll-off success, roll-off failure and recovery confirmation. The results show that the number of cars in track 1 converges from 5 to 7, the unrecoverable failure probability is 0.48%±0.01%, and the completion probability of Train(2) reaches 0.9558 at 330min. Disturbance experiments show that the arrival rate and recovery rate will change the controller state occupancy time and the tail train completion probability. The results show that statistical model checking can provide quantitative verification basis for reliability evaluation of railway marshalling yard operation plan.
