Formal Modeling and Analyzing of CTCS Radio Communication Based on Stochastic Petri Nets
Xiaohui Hu · Journal of the China Railway Society · 2011
The wireless communication system of CTCS-4 is a dynamic,complex and distributed system.It is significant to implement formal verification of properties and final realization of the CTCS communication system.The paper gives careful consideration to formalized modeling and reliability analysis of the wireless communication system of CTCS under the condition of moving blocks with high-speed trains.Then two models are established,one is for the mechanism of wireless communication with the Stochastic Petri Net,the other is for failure and recovery behavior of GSM-R when trains are communicating with RBC.Meanwhile,the representation for locating of communication faults is shown and the reliability of the communication system of GSM-R is analyzed by using the tools of TimeNET to draw the corresponding conclusion.Performance evaluation shows that the handover dependability of 99.45% and connection loss rate of 10-2 times per hour take place at the train speed of 500 km/h.The GSM-R requirements are seen to be satisfied through comparison with the analysis results.