基于SPN的CTCS无线通信形式化建模与分析

摘要

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.%CTCS-4列车运行控制系统是基于无线通信传输信息的系统,其无线通信系统是一个动态、复杂的分布式系统,正确的形式化验证对于其性质和最终实现具有重要意义.本文主要考虑高速列车在移动闭塞区间条件下CTCS无线通信的形式化建模和可靠性分析,建立随机Petri网(SPN)表示的CTCS无线通信机制模型和列车与无线闭塞中心通信的GSM-R故障恢复模型,给出对通信故障定位的表示方法,并采用TimeNET仿真工具对GSM-R通信系统的可靠性进行分析得出相应结论.分析结果表明,列车在500 km/h的速度下,越区切换成功概率为99.45%,连接丢失概率为10-2/h.最后,本文将分析结果与GSM-R的技术标准进行比较,说明其可靠性满足规范要求.