基于着色Petri网的铁路时间同步协议建模及安全性分析

针对Autokey模型的铁路时间同步协议安全性问题,提出利用着色Petri网对协议进行安全性分析。剖析Autokey模型的铁路时间同步协议序列及其执行流程;重点针对其认证阶段,分别构建正常认证和加入中间人入侵的着色Petri网模型,分析中间人入侵时协议认证过程的不安全状态,建立模型状态方程;应用逆向状态分析法对铁路时间同步协议认证过程的安全性进行分析,得到中间人在认证阶段攻击协议的实施序列。研究结果表明:基于Autokey模型的铁路时间同步协议的认证过程是不安全的。     

一种改进型网络时间协议在TDCS/CTC系统的应用研究

由于列车运行速度较高,短时间内列车跨线跨区行驶,铁路信号设备时间统一显得尤为重要,而现有的铁路时间同步方法无法满足目前对于同步精度的要求。为了解决上述问题,采用网络时间协议NTP进行铁路TDCS/CTC系统的时间同步,但网络发生拥挤时,会影响同步精度。为了更精确地同步系统时间,保证行车安全,并使列车在速度进一步提高时,仍能满足时间同步的精度要求,本文提出一种改进型NTP协议,对协议的算法进行仿真分析。仿真结果表明该算法能够有效提高时间同步精度。     

网络时间协议简析

主要对时间同步系统中使用的主要协议网络时间协议（NTP）进行简要介绍,对NTP的基本功能和工作机制进行了简要分析。     

下一代高速铁路LTE-R时间同步网协议脆弱性分析

铁路无线通信系统时间同步网络,是保障行车安全和提高铁路运营效率的重要基础。针对下一代高速铁路LTE-R自身全IP化架构在使用精确时钟PTP时间同步协议过程中易受到ARP攻击的问题,提出基于随机Petri网(SPN)的LTE-R时间同步网协议脆弱性分析方法。建立了ARP攻击状态下LTE-R时间同步网协议脆弱性分析SPN模型;通过马尔科夫链同构的方法,得到ARP攻击下LTE-R三级时钟节点实施速率与PTP协议同步正常、异常之间的关系曲线;定量得到了影响LTE-R时间同步网协议脆弱性的关键因素。研究结果为GSM-R时间同步网络向LTE-R安全演进提供了一定的理论参考依据。     

基于随机Petri网的铁路时间同步网协议脆弱性分析

针对铁路时间同步网的时间同步协议脆弱性问题,提出将随机Petri网(SPN)和马尔科夫链相结合进行协议脆弱性分析。剖析铁路时间同步网的结构、协议执行流程,建立铁路时间同步网中时间同步协议在中间人攻击作用下的SPN模型;分析影响协议脆弱性的相关状态,得到协议脆弱性相关状态的实施速率与协议正常结束状态和异常结束状态稳态概率之间的关系曲线;确定影响铁路时间同步网中时间同步协议脆弱性的具体因素。研究结果可为维护铁路时间同步网及制定相应性能指标提供借鉴。     

基于半马尔可夫过程的铁路时间同步网协议安全量化分析

针对基于Autokey模型的铁路时间同步网协议安全性问题,考虑时间同步协议在攻击行为下的状态驻留时间为非指数分布,提出基于半马尔可夫过程的铁路时间同步协议的安全性量化分析方法。剖析基于Autokey模型的铁路时间同步协议序列执行流程,建立带有网络攻击行为的铁路时间同步协议完整性验证过程的状态变迁模型。分析协议的不安全状态与协议相关安全性指标之间的关系,得到协议各安全性相关指标与协议不安全状态的变迁概率和状态驻留时间之间的关系曲线,分析影响铁路时间同步网协议安全性的关键因素。研究结果可为铁路时间同步网信息安全维护提供借鉴。     

基于CPN的联锁系统选岔网络建模及验证

在详细分析联锁系统选岔电路的前提下,抽象出选岔网络的联锁逻辑条件,并采用有色Petri网(Colored Petri Net,CPN)为其建立形式化验证模型,同时采用CPN TOOLS对所建立的模型进行仿真及状态空间分析,结果表明所建立的模型能够很好的描述选岔网络的工作状态。     

基于有色Petri网的车载设备模式转换测试序列生成方法

为高效、自动生成覆盖车载设备所有转换路径的测试序列,根据《CTCS-3级列控系统系统需求规范》,首先基于有色Petri网构建车载设备模式转换(MTCPN)模型,并采用ASK-CTL公式和非标准状态空间查询法对MTCPN模型进行分析和验证,然后根据车载设备模式转换规则,将车载设备的工作模式及其转换路径映射为有向图,采用中国邮路算法求解有向图,生成1条最优邮路,并对该邮路进行二次优化,生成车载设备模式转换的测试目标序列集;将测试目标序列作为MTCPN模型的输入,仿真生成满足全路径覆盖准则的可执行的测试序列集和XML文件。验证结果表明:基于有色Petri网的测试序列生成方法能够满足测试需求,并且避免了既有方法的状态空间爆炸和搜索死循环问题,提高了测试效率。     

铁路信号控制逻辑的有色Petri网描述方法

铁路信号逻辑控制关系的形式化描述对实现铁路信号设备计算机控制系统的研制开发具有十分重要的意义.形式化的描述不但可以便于计算机实现具体的逻辑控制,同时也可以提高计算机程序的可靠性.对这些逻辑关系精确地描述之关键在于选择恰当的描述语言.本文利用有色Petri网的特点结合一些铁路信号设备的变化规律给出了相应的有色Petri网描述,并针对一种简化的区间自动闭塞的控制逻辑介绍了用有色Petri网建模的基本方法和有色Petri网模型的分析过程.     

基于UML与CPN的CTCS-3级列控系统建模与验证方法研究

CTCS-3级列控系统安全功能极其复杂,为保障其正常运转,有必要对列车运行控制系统的建模与验证进行深入研究。在分析了UML建模图和有色Petri网优缺点的基础上,提出了UML和有色Petri网(CPN)相结合的建模与验证方法,并应用在CTCS-3系统中,对CTCS-3级列控系统的建模与验证具有积极的研究意义。     

判决PN机理论及其在入侵检测中的应用

论文针对攻击行为的知识表示和智能分析展开研究,利用Petri网理论和人工智能技术,建立适合攻击行为分析与检测的理论和方法。提出一类Petri网子类型判决PN机和着色判决PN机作为攻击行为的描述模型,利用其运行机制检测攻击,并使用着色判决PN机的有色合成解决模式关联的问题,同时     

有色Petri网在平交道口安全性分析中的应用

平交道口是铁路和公路的交汇点，一旦发生交通事故，不仅影响整个交通运营效率，还会引起严重的人员伤亡，因此，平交道口的安全性对轨道交通和公路交通都至关重要。为了分析平交道口的安全性，提出基于模型的方法对平交道口进行建模和基于模型检验的方法对平交道口的安全性进行分析。应用有色Petri网作为分析工具，建立平交道口部分功能的模型，设计平交道口部分安全分析的算法，验证了有色Petri网在平交道口安全性分析上的可行性。     

基于通信的列车运行控制系统安全通信协议的性能分析

安全通信协议是保证基于通信的列车运行控制系统中通信安全的主要因素,其性能分析具有重要意义。针对基于通信的列车运行控制系统安全通信协议,选择分层赋时有色Petri网(CPN)对其进行研究,建立状态转换模型与包含数据延时和信道故障的模型,通过改变数据延时的概率和信道无故障的概率,对安全通信协议的稳定性和失效率进行仿真,仿真结果对安全通信协议的设计有一定的参考意义,用概率论与数理统计知识对仿真结果进行分析,分析结果体现数据延时和信道故障是如何影响安全通信协议的性能的。分析结果表明基于通信的列车运行控制系统安全通信协议是合理的。     

部分可观Petri网系统的在线故障诊断方法

针对Petri网系统故障检测与诊断过程中存在状态枚举及随后的状态爆炸问题,采用整数线性规划方法,提出了Petri网系统的在线故障诊断算法。算法将故障表示为Petri网模型的不可观变迁,定义了故障诊断器函数,通过可观的变迁序列,诊断系统行为是否出现故障。该算法避免了状态空间爆炸,降低了在线运算量的复杂性。以地铁列车进出站系统为实例,对地铁列车进出站系统进行含不可观变迁Petri网建模,应用提出的算法对铁列车进出站系统故障进行诊断。试验表明,该算法能有效应用于地铁列车进出站过程在线故障诊断。     

一种层次化CPN模型及其在给排水系统中的应用

先分别介绍了Petri网和面向对象技术,提出将高级Petri网和面向对象技术相结合构成层次化的面向对象有色Petri网（HOCPN）模型。该模型综合了面向对象技术和Petri网的优势,实现了对较为复杂网络的建模,从而可以进一步地实现对复杂网络进行验证。最后,将该建模方法在给排水系统中进行实际应用。     

列车区间运行安全的Petri网模型研究

鉴于我国铁路列车行车事故多发生在区间运行过程中,以及列车在区间运行的动态特性,利用Petri网具有强大的功能描述及分析系统动态变化的特点,建立了列车区间运行系统的动态Petri网模型。通过对该模型合理性的论证,并运用此模型对实际事故案例进行分析,表明所建的列车区间运行安全Petri网模型是合理的。     

无线列控系统安全通信协议性能评价规则的制定方法

针对传统方法在评价列控系统安全通信协议性能时存在只能定性不能定量和对评价人员掌握评价尺度有差异考虑不足的问题,基于利用有色Petri网模型对列控系统安全通信协议性能的仿真结果,运用决策论中的概念格理论对有关安全通信协议性能(包括建立安全链接需要的时间和传输信息需要的时间)的仿真数据进行分析,研究制定安全通信协议的性能评价规则。运用Dempster-Shafer理论,分析评价人员应用给出的安全通信协议性能评价规则对安全通信协议性能进行评价所得评价结果的不确定性,以验证所提出安全通信协议性能评价规则的可行性。结果表明,使用所制定的安全通信协议性能评价规则克服了传统方法的不足,而且以概率的形式定量表示安全通信协议的性能,可使评价结果更全面也更具有说服力。     

ETCS-2级列控系统RBC交接协议的形式化分析

RBC(无线闭塞中心)交接协议是影响ETCS-2级欧洲列车运行控制系统的控制精度、效率、可靠性和安全性的主要因素之一.对该协议的形式化分析可为我国CTCS-3级列车运行控制系统的规范制定和系统研发提供参考.随机Petri网语义清晰、语法严谨,并且具有良好的数学理论支撑,与仿真手段相比能够得出更加可信的定量分析结果.本文选择随机Petri网(SPN)这一形式化语言对RBC交接协议进行研究,综合信道突发降质、GSM-R小区切换、链路中断等故障因素,针对两种协议方案分别建立RBC交接失败概率模型,分析列车运行速度、RBC重叠范围对交接成功概率的影响.结果表明基于两个车载电台、切换时能同时与两个RBC通信的RBC交接协议能够更好地保证列车交接过程的安全性,对行车效率的影响比较小.     

基于Petri网技术的动车组检修作业工作流系统研究

针对目前动车组检修业务,抽象出作业过程规则,并建立动车组检修作业工作流程.通过工作流和Petri网的相关理论对该工作流进行建模,并利用Petri网技术分析方法,从模型的正确性分析和性能评价两个方面对所建立的Petri网模型进行分析.     

城市轨道交通综合监控系统时钟同步方案研究

介绍了城市轨道交通综合监控系统对时钟同步的要求和网络时间协议(NTP).结合北京地铁5号线的实际应用案例,重点对中心级和车站级综合监控系统的时钟同步方案进行了分析和研究.实际应用表明:在中心级综合监控系统中,冗余时钟源对时方案优于单时钟源对时方案;在车站级综合监控系统中,相对于独立时钟源方案,共享时钟源方案具有明显的优势.基于NTP的时间同步方法为综合监控系统提供了统一、高效、精准的时钟,经北京地铁5号线多年运用,实证其为运营的可靠性提供了基础保障.