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