我国CTCS-3级列车运行控制系统是基于无线通信GSM-R的列车运行控制系统。GSM-R系统为列车运行提供安全、可靠的数据传输通道,实现了车地间双向通信。为确保CTCS-3级列车运行控制系统数据传输的安全性和可靠性,用于抵御各种安全隐患的车地通信协议的正确性及合理性显得尤为重要。论文首先阐述了CTCS-3级车地通信协议的系统结构,根据数据传输安全相关需求,详细分析了CTCS-3级车地通信协议的安全通信标准。然后,论文选用形式化描述语言SDL和其支撑工具Telelogic TAU,对CTCS-3级车地通信协议状态机进行形式化描述,建立SDL系统模型,并对其进行协同仿真和遍历验证,生成消息序列流图MSC和错误报告,并通过验证说明了该SDL系统模型的准确性。最后,论文在所建SDL系统模型的基础上将其自动转换为C代码,并最终应用与CTCS-3级车地通信协议软件中,该软件已经服务于CTCS-3级列控系统测试评估认证平台。论文将标准描述语言SDL引入CTCS-3级列控系统,以形式化描述技术为主线对CTCS-3级车地通信协议进行描述与实现,不仅能够从协议描述上消除语言的二义性,而且能够减少实现通信软件的错误,缩短开发周期,降低开发难度。基于SDL协议设计方法实现的CTCS-3级车地通信协议软件在防护数据传输的安全性和可靠性上也有很好的保障,将其成功应用于CTCS-3级列控系统测试评估认证平台能够进一步证明该方法的实用性,对CTCS-3级列控系统的验证和评估测试具有重要的现实意义。