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

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

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

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

大型客运站最高聚集人数仿真计算方法研究

铁路客运站最高聚集人数传统计算方法采用静态公式计算,忽略了车站功能布局、客流组织方案与最高聚集人数的互动影响。在研究旅客最高聚集人数形成机理的基础上,提出并证明3个规律,揭示最高聚集人数影响因素的作用规律、最高聚集人数的周期特性和出现时间;通过对15万条现场统计数据的拟合分析,提出旅客提前到站时间分布密度函数;运用车站客流组织仿真系统,研究提出车站最高聚集人数的仿真计算方法,并采用北京南站数据进行验算。结果表明,该方法可为车站方案设计、运营管理方案编制提供参考。     

基于模型选择和优化技术的自动驾驶制动模型辨识研究

本文结合城市轨道交通列车自动驾驶系统实测数据,对电动客车制动模型的类型和参数的辨识进行较为深入的研究。首先,在分析最大制动率条件下实测制动数据后,对列车制动模型类型进行研究。然后,应用非线性优化技术在不同模型种类、有无参数范围约束等情况下,对制动模型进行辨识,并根据模型选择技术获得最佳制动模型及其参数。最后,研究不同制动率下列车制动模型的一致性,并基于模型选择技术给出制动率和制动减速度之间的模型。     

基于脚本技术的高速铁路列控中心系统安全性自动化测试研究

列控中心系统是实现高速铁路安全运行的关键设备。自动化的黑盒测试是验证其系统功能和确认系统满足系统需求,具有足够安全性防护能力的重要手段。脚本技术是实现软件测试自动化技术的有效方法。测试脚本语言是脚本技术的核心,但是目前没有专门针对列控中心测试的脚本语言。本文结合列控中心测试的特点,提出一种测试策略,设计了场景-事件驱动的测试脚本语言SED_TSL。在本文提出的测试策略中针对安全防护功能,以实际运营场景为核心,利用测试脚本语言SED_TSL定义正常场景与故障场景,测试序列与测试用例,仿真环境,形成分级测试脚本。通过场景变换控制测试逻辑与流程,触发仿真事件加载测试用例实现系统的功能性与安全性测试。本文对测试脚本语言SED_TSL与基于SED_TSL的自动化测试环境的实现机制进行阐述,并实现了基于SED_TSL的高速铁路列控中心系统自动化测试环境,投入到铁道部的列控中心产品制式检测中。实际应用表明:测试脚本语言的描述能力与自动化测试环境符合测试需求,有效地实现了列控中心产品的功能与安全性测试。     

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

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

高速列车进入有缓冲结构隧道的压力变化研究

采用高速列车空气动力学模型实验对高速列车在进入带缓冲结构隧道过程中瞬变压力传播机理进行研究。实验结果表明,缓冲结构能够减缓隧道内瞬变压力。其原因在于:缓冲结构横断面积逐渐由大变小,阻塞比逐渐由小变大,延长了压力上升时间,降低了压力梯度;另一方面,由于压缩波在缓冲结构和列车、隧道之间多次反射,降低了压力峰值。在M.S.Howe提出无缓冲结构下最大压力波变化理论基础上提出有缓冲结构时隧道内最大压力和最大压力梯度变化规律计算公式。所得结论可为隧道空气动力学研究提供参考。     

空调导流罩对列车气动阻力影响的研究

对空调导流罩的原始结构进行了外流场分析,得到了在350 km时速下原空调导流罩的外表面压力分布和速度场分布,通过对速度的流向分析,对空调导流罩的外形结构进行了优化。利用风洞试验对优化前后2种方案进行了气动阻力系数对比,结果表明,优化后的空调导流罩使头车的气动阻力减小了2.6%,改善了车辆的空气动力学性能,并为高速列车空调导流罩的基本造型设计提供了理论依据。     

提高列车交会的安全性设计及仿真分析

以CRH2—300型高速动车组为例,建立了流固耦合模型,分析了列车交会过程中车间减振器和空气弹簧横向跨距对行车安全性的影响。研究结果表明,增加车间减振器和增大空气弹簧横向跨距对改善列车交会过程中的安全性有比较明显的效果。为了保证高速列车的行车安全,安装车间耦合减振器和适当增加二系侧滚角刚度是很有必要的。     

城市轨道交通换乘站的列车衔接时间优化

城市轨道交通网络化运营条件下,协调优化各线列车运行计划,使不同线路的列车在换乘站形成良好衔接,能够缩短乘客的换乘等待时间。合理的换乘站列车衔接时间是编制网络列车运行计划的基础。基于乘客的换乘等待心理和列车运行延误的随机性特点,确定了列车衔接时间的组成。分析了列车运行延误对列车间衔接关系的影响,建立了换乘等待时间的费用函数。在此基础上,提出了换乘站列车衔接时间的优化模型,并给出了具体算例。该模型可为列车衔接计划中安排的换乘衔接关系确定最佳的列车衔接时间,为网络列车运行计划的协调编制提供指导。