基于CPTA实现报文数据与车载系统契约关系的研究

线路数据是驱动列控系统安全运行的基础。目前,有关列控数据安全的研究多集中于验证数据自身的完整性与合理性,却很少关注数据与其宿主系统间的契约关系,这可能会忽视由于数据没有满足宿主系统需求而产生的安全隐患。针对此问题,分析车载ATP在计算动态监控曲线过程中对报文语法、语义和时效性三方面的需求,并将其形式化为PVS公理,作为列车状态迁移条件来构建报文-车载CPTA契约模型,借助PVS定理证明工具证明该契约模型的正确性。实验结果表明,基于报文-车载的契约模型能够实现高效且可靠的报文验证,从而减少由于报文数据失效而引发的列车异常制动或降速的次数。     

计算机联锁控制逻辑的模型检验方法

描述了符号化模型检验策略和相应的工具软件SMV,通过该工具验证了铁路计算机联锁控制逻辑的设计符合其安全规范,最后分析了模型检验面临的困难以及今后的努力方向.     

CBTC数据通信系统性能分析模型及应用研究

数据通信系统DCS(Data Communication System)是影响CBTC系统的控制精度、效率和安全性的主要因素,其通信性能的仿真、验证对于CBTC系统的研发和改进有重要意义。本文介绍利用OPNET模拟自主研发的安全通信协议和构建DCS性能仿真研究平台的方法,给出安全通信协议有限状态机模型和可配置的通信子系统节点通用模型,研究平台可用于分析安全协议在整个通信网络上的总体性能。给出利用节点模型建立整个DCS通信网络的算例和网络性能的仿真结果,实验结果表明,通信周期不完全同步可以减小报文时延,网络出现故障后,改变生成树根节点位置使最大报文时延增加近34%。     

列车定位轨道电子地图数据约简算法研究

高效、高精度的轨道电子地图是实现列车定位及列车运行控制的重要基础。为了提高轨道电子地图数据的存储及使用效率,在地图生成过程中需要在保证精度的前提下对测量数据进行约简。本文在实测数据的基础上分析轨道地图测量数据特性,采用小波变换及距离判别的方法对异常测量数据进行剔除,提出一种基于垂距判定和三次B样条曲线拟合的数据约简算法用于地图生成。该算法利用垂距判定方法从异常值剔除的原始数据中选取一定数目的测量点构成轨道特征点集,并对其进行三次B样条拟合,通过对拟合曲线进行误差判别修正和补充特征点,完成数据最终约简及轨道地图生成。青藏线实测数据验证结果表明,在合理选择垂距限差的情况下,该算法能够有效约简原始地图测量数据,并保证所生成地图的精度水平。     

CTCS-3级列控系统规范的建模与形式化验证方法研究

CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节。然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验证显得十分必要。本文提出CTCS-3级列控系统规范建模与形式化验证方法,此方法的特点是能够在系统规范、模型、验证工具以及验证结果之间建立一条跟踪链,从而始终保证系统规范、模型及程序代码之间的一致性。结合笔者运用此方法对CTCS-3级列控系统规范建模与形式化验证的实践,证明这种方法是可行的、高效的。     

高速铁路列控系统运营场景实时性的建模与验证

高速铁路列控系统是一个典型的分布式实时系统,其时间约束主要反映在运营场景中子系统之间的交互过程中。时序逻辑的扩展方法并不能完全满足描述分布式实时系统性质的需要,并且随着系统的复杂性提高,列控系统运营场景中诸如超时、期限、直到…才等形式化描述与验证上存在不足。本文提出一种适合于列控系统场景建模与验证的方法,其核心思想是使用混合通信顺序进程HCSP(Hybrid Communicating Sequential Process)形式化描述分布式实时系统模型,提出转换规则,转换成时间自动机网络模型并进行自动验证。最后通过对典型场景无线闭塞中心RBC(Radio Block Center)切换的相关属性进行建模与验证,分析证明方法的有效性。     

基于位置的CBTC系统无线局域网切换机制

目前的城市轨道交通CBTC车地通信系统大多采用无线局域网技术。针对同时存在无线自由波和漏泄波导车地通信技术的CBTC无线局域网车地通信系统,提出一种基于位置的无线局域网切换机制。在无线自由波覆盖区段,移动台在确定的位置直接发起重关联请求,而不需要进行探询扫描新AP的过程。而在漏泄波导覆盖区段,通过改变移动台扫描的信道数和最大信道扫描驻留时间,同样明显减小了切换时延。该方法不仅适用于无线自由波的覆盖区域,也可以应用于漏泄波导覆盖的区域,能够减少CBTC车地通信系统中的切换时延。     

运行时验证及其在列车运行控制系统中的应用

运行时验证是一种将模型检验方法与测试相结合的轻量级验证技术,它能够有效地降低系统验证的复杂度,提供系统运行阶段的安全保障,因此在安全苛求系统的验证领域有着极其重要的应用。本文提出一种基于三值逻辑的有限轨迹LTL可执行语义,允许"真"和"假"以外的逻辑值来显式的刻画验证过程中可能出现的非确定性,从而使得验证的结果更加精确。针对新的LTL语义给出了基于公式重写的运行监控算法和近似优化策略,并结合欧洲列车运行控制系统的实例,分析探讨了该方法在轨道交通控制领域的应用。     

城轨虚拟编组关键性能指标及技术探讨

列车虚拟编组技术能够实现车辆资源的高效灵活利用,是解决轨道交通客流时空分布不均衡问题的有效方法,已成为国内外的研究热点。既有研究借鉴了汽车编队追踪的思路,主要关注于列车稳定追踪的相关方法,未能完全适应轨道交通的实际需求。针对城市轨道交通(简称“城轨”)虚拟编组研究的需要,深入分析城轨列车运行的特征,在此基础上总结提出包括站台停车时间差等在内的城轨列车虚拟编组应符合的技术性能指标;其次,针对虚拟编组的技术特征,提出包括大小交路和Y型线路等适合列车虚拟编组的潜在应用场景,并对实现虚拟编组的关键技术及其原理进行介绍,可为城轨列车虚拟编组研究提供参考。     

基于元模型的通用性列控仿真平台基础环境研究

为实现列控仿真系统可重用性、可扩展性及可组合性的目标奠定底层基础,提出将列控系统分为控制器和控制对象,即列车控制策略和列车运行基本环境,在列控仿真系统中将控制器和控制对象分离设计。通过总结不同轨道交通系统运行的共性特征,将线路拓扑结构、列车模型和驾驶模型作为列车运行基础环境的3部分,采用元模型思想形式化描述列车运行基础环境的3部分,设计了基础线路数据库与仿真线路拓扑结构映射的关键算法和列车运行规则。采用高速铁路线路数据实现了列车运行基础环境,结果表明:所做研究在满足列控仿真平台需求的基础上,达到了列控仿真系统平台运行基础环境通用性目标。