论文研究CTCT4级安全通信协议的形式化建模与验证.pdf

CTCS-4级列车运行控制系统是基于无线通信GSM-R传输信息的系统，而GSM-R系统是一种开放传输系统，它不能满足列控系统这种安全苛求系统的需求。主要根据GSM-R系统现有的安全威胁和应该采取的安全措施，引用一种改进的NSSK安全协议来保障车载设备与RBC间安全通信，并利用形式化建模语言CSP和模型检测工具FDR对其建模和验证。