原文传递
基于有色Petri网的STP安全通信协议设计与验证
| 论文题名： | 基于有色Petri网的STP安全通信协议设计与验证 |
| 关键词： | STP系统;安全通信协议;自然语言;有色Petri网;形式化验证 |
| 摘要： | 无线调车机车信号和监控系统(STP)是保证站内调车作业安全、提高调车作业效率的重要设备。近年来，随着站内调车作业任务量和复杂度不断加大，对STP系统安全性要求也在不断提高。据此，本文提出一套适用于STP系统的安全通信协议，并基于有色Petri网进行形式化建模与验证。结果表明所设计的STP安全通信协议符合标准En50159-2010具备安全功能，可以抵御信道中的传输威胁。主要研究内容如下: (1)分析STP系统安全通信需求。根据STP系统功能结构、现有车-地通信方式，以及En50159-2010标准的相关要求，分析STP系统对安全通信协议的总体需求。 (2)采用自然语言设计安全通信协议。参考EuroRadio和RSSP-Ⅱ现有安全通信协议，并在其基础上加以改进，采用层次化架构设计安全通信协议，并针对不同层采用不同的安全防护措施，设计适用于STP系统车-地通信需求的安全通信协议。 (3)采用有色Petri网对安全通信协议进行形式化建模。基于协议工程理论，依据STP通信系统结构以及安全通信协议的层次化功能结构，采用有色Petri网依次建立安全通信协议运行载体-安全层的基本接口模型和防护机制模型。 (4)对协议进行形式化验证与性能仿真分析。本文采用基于时序逻辑ASK-CTL的模型检验法并结合状态空间分析法和性能仿真法，对STP安全通信协议进行了全面、综合的验证与分析。时序逻辑模型检验法的引入实现了对安全通信协议安全相关特性的验证，弥补了系统模型仅靠状态空间分析和性能仿真验证的不足之处。 |
| 作者： | 李堃 |
| 专业： | 交通信息工程及控制 |
| 导师： | 张雪松 |
| 授予学位： | 硕士 |
| 授予学位单位： | 中国铁道科学研究院 |
| 学位年度： | 2018 |
| 正文语种： | 中文 |
检索历史
应用推荐
