CTCS-3级列控系统规范建模与验证

结合统一建模语言UML与符号模型检验SMV形式化方法,提出需求规范严格建模和验证方法。利用需求管理工具,保证了模型和规范的一致性和对规范的覆盖性,同时实现了规范验证结果对模型、转换规则和规范的跟踪。给出了CTCS-3级列控系统严格建模与验证的方法体系和流程,并以CTCS-3级列控系统需求规范中的模式转换部分为例,说明了规范的建模、验证和分析过程。     

基于GPS与惯性测量单元的列车组合定位系统

采用GPS接收机及惯性测量单元构成列车组合定位系统,系统包括传感器输入层、故障检测与隔离层、数据融合层和输出层4个部分。给出GPS接收机、惯性测量单元等定位传感器的位置解算方法;设计采用H∞鲁棒滤波方法的数据融合算法;采用小波变换方法进行组合系统故障检测,确定故障隔离及系统重构策略。对列车组合定位系统进行现场测试和仿真验证结果表明:在复杂的列车运行环境及干扰条件下,该系统能够实现高精度高可靠性的列车定位;定位误差较采用传统的Kalman滤波方法更为稳定;组合系统能够有效实现故障检测并根据故障隔离策略重构系统,保证定位输出的连续性,保障系统安全;具有较高的适应性和实际应用价值。     

CBTC越区切换中断时间分析

基于通信的列车控制(CBTC)系统采用IEEE802.11标准作为无线通信传输协议。根据IEEE802.11标准中规定的越区切换流程,采用移动通信系统越区切换中断时间的计算方法,推导出越区切换中断时间与列车运行速度的关系表达式。采用此关系表达式进行理论计算的结果显示,在发射功率为17 dBm,发射和接收天线增益均为10 dB,发射与接收端损耗均为5 dB的条件下,典型行车速度为50,70,90 km.h-1时,越区切换中断时间应分别控制在224,160和124 ms以内才能够保证通信持续正常。建立2列列车追踪运行模型,仿真不同越区切换中断时间的后车运行曲线。仿真结果显示:列车以25 m.s-1(90 km.h-1)的速度行驶时,越区切换中断时间在130 ms以内能够满足列车通信的需求;验证了CBTC越区切换中断时间与列车行驶速度的关系表达式是合理的。     

拉索劣化性能研究

通过对斜拉桥拉索劣化或失效案例的剖析，介绍了拉索劣化性能以及最新研究成果。分析归纳了当前拉索腐蚀失效的研究现状以及相关试验方法。最后提出了目前在拉索性能研究中存在的局限以及迫切需要解决的问题。     

一种信息时效性判定算法在列控系统中的应用

在列控系统中各种信息都有其寿命周期,这些信息都必须在允许的时限内传递给信息的使用者.列控系统中信息的时效性对系统安全有重要影响,超时的信息如果被系统使用,则可能出现安全隐患.因此如何判定信息的时效性是系统设计人员亟待解决的问题.本文综合目前列控系统中信息传输延时的因素,引入一种信息时效性判定算法.概述算法的基本原理,描述算法的流程.用定理证明的方式,论证它的正确性和安全性.通过计算机仿真,评估算法的快速性和稳定性,并且分析算法的可用性.研究结果表明,这种信息时效性判定算法在理论上是安全的,在实际应用中是可用的,即使在要求更为苛刻的参数条件下,其可靠性可达到99.15%,能够满足列控系统的要求.     

多端口形式化测试自动生成方法在CTCS-3车载系统中的应用

针对CTCS-3列控系统测试中普遍存在的需要多个端口协同测试的问题,在时间输入输出自动机(TIOA)的基础上,提出端口标记的时间输入输出自动机(LpTIOA).LpTIOA除在模型中能够反映系统的时间约束特性外,还能反映系统输入输出行为对应的端口信息,利用这些信息对基于覆盖度的搜索算法进行相应改进,形成包含端口信息的测试自动生成算法,用于生成满足给定覆盖度标准的测试套.文中还描述了运用UPPAAL工具对LpTIOA模型实现建模的方法,并运用COVER工具实现对经过UPPAAL验证的CTCS-3级车载系统LpTIOA模型的测试套自动生成.     

基于UML的CTCS-3级列控系统需求规范形式化验证方法

采用UML与符号模型检验相结合的方法,对CTCS-3级列控系统需求规范进行形式化验证.使用引入事件、可见变量抽象的方法,对需求规范UML模型进行扩展和抽象.根据转换规则,建立需求规范的NuSMV模型,并对NuSMV模型进行领域无关特性和领域相关特性的验证,通过反例对错误进行追踪、定位和修改.以需求规范中的模式转换为例,采用给出的形式化验证方法对其进行验证,验证结果确认模式转换满足活性、转移性、无死锁性、确定性及安全性的要求;验证过程表明UML与符号模型检验相结合的方法适用于CTCS-3级列控系统需求规范的验证.     

低成本列车组合定位系统容错算法设计

列车实时定位是列车控制系统的重要环节。在安全苛求的现代列车控制系统中,列车定位系统需要在实现高精度列车定位的同时具备容错能力,以保证系统安全。针对列车定位的安全性需求,从保障列车定位系统的容错性能出发,利用低成本GPS接收机、惯性测量器件以及里程计等定位传感器构成列车组合定位平台,给出列车组合定位系统的结构与功能,将小波变换方法用于组合系统故障检测并制定相应的故障隔离策略,以H∞鲁棒滤波为基础设计联邦结构的多传感器容错信息融合算法用于定位计算。利用自制轨道推车进行的实验及仿真结果表明,组合定位系统能够满足列车定位的精度要求,并具有较强的容错能力,能够在不同定位条件下保证定位高效与安全。     

基于SPN的越区切换模型分析

CTCS-3列车运行控制系统是中国列车控制系统(CTCS)的重要组成部分之一,它采用GSM R实现地面一列车间连续、双向的安全信息的无线传输.对于GSM-R而言,移动台的越区切换必然引起通信连接的暂时中断.由于安全数据传输直接影响行车安全,为保证其传输的可靠性,必然要求更短的切换时间和更高的切换成功率.本文研究安全数据通信在越区切换时的传输可靠性,并对越区切换过程进行随机Petri网的建模和分析.给出列车速度与越区切换成功率的关系,以及列车在350km/h的速度下,越区切换时间与越区切换成功率之间的关系.最后,本文将分析结果与CTCS-3需求标准进行了比较,说明其可以满足要求.     

路在脚下延伸——记第九届詹天佑铁道科学技术奖成就奖获得者、中国铁道科学研究院主任研究员段武

受益于名师引路、成功于勤奋钻研.三十年前走出校门的段武,从那时开始,他就在铁道信号专业领域里长途跋涉、孜孜以求.天道酬勤、事遂人愿.如今,他已成为一位出类拔萃的铁路专业技术带头人,成为一名屈指可数的铁道装备学科带头人.对此,段武颇有感慨地说:"我们的所有成果都是在前辈研发的基础上取得的,有了一,才会有二.任何事物发展都是这个规律."