Analysis on EURORADIO safety critical protocol by probabilistic model checking

The EURORADIO system provides communication services for safety-related application processes using open network. The EURORADIO protocol controls the establishment of safety connection between on-board and trackside, and the time for establishment of safety connection is a key parameter to communication system. After describing the requirements in the EURORADIO specification, the probabilistic model checking tool PRISM is used to implement a formal analysis on the property of safety connection, combing the stochastic characters of communication channel. Verification results show that, when the protocol is applied in China Train Control System level 3 in case of 0.01 of message loss, the probability for establishment of safety connection in 8.5 seconds is 0.96059, and the probability is 0.99844 after establishing safety connection twice, it can fulfill the requirements of the specification.