CTCT-4级安全通信协议的形式化建模与验证

摘要：

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

关键词：GSM-R、安全协议、通讯顺序进程(CSP)、故障、偏差、精炼检测器(FDR)

分类号：TP391.9(计算技术、计算机技术)

资助基金：国家自然科学基金No.61163009。

在线出版日期：2014-02-27（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：81-85