基于Event-B的双机热备平台测试序列自动生成方法

为了确保双机热备平台满足相应的功能需求，需要对其进行功能测试。采用基于模型的测试方法，可以有效地避免人工手动生成测试中存在的不足，提高测试效率。利用Event-B方法对双机热备平台进行形式化建模，通过证明验证模型的正确性，并进一步利用Ll算法生成基于模型、满足平台测试需求的测试序列集，对于确保测试过程的完备性、提高测试效率有一定意义。     

热备动车组配置方案优化模型

热备动车组的配置方案影响热备动车组的救援效率,对保证铁路正常运行秩序起着重要作用。针对配置方案中热备动车组数量的确定和备用地点的选择,以全面覆盖铁路事故风险为约束,分别以热备动车组平均响应时间最短及配置成本最少为目标,建立热备动车组配置方案优化的多目标规划模型,并设计分步搜索的禁忌搜索算法对多目标模型的Pareto解集进行求解,最后结合算例,验证了模型和算法的可靠性。研究结果表明,得到的热备动车组配置方案能够满足决策制定者的不同偏好,热备动车组配置数量和地点协同优化的方案较两者分步优化更能提高热备动车组应急效率。     

基于UPPAAL的列车自动防护系统形式化建模与验证

本文分析列车自动防护(ATP)系统的结构和功能需求,建立系统的时间自动机模型,采用UPPAAL模型验证工具对模型的活性和安全性进行验证.结果表明,采用时间自动机对安全苛求实时系统进行建模与验证,可以有效地保证系统的可靠性和实时性.     

基于备选集的高速铁路列车开行方案优化方法研究

高速铁路成网后列车开行方案的编制面临新需求,不仅要紧密联系既有线运输,而且必须适应大规模全网优化的需要。本文提出基于"备选集"的高速铁路列车开行方案优化方法,列车开行方案的编制分两阶段实现,使其具有很强的可操作性并符合实际应用特点:首先根据一定原则生成备选集,得到最有可能开行列车的集合作为列车开行方案优化的解空间;其次结合多商品流问题,建立基于备选集生成列车开行方案的混合整数规划模型,求解列车开行方案的同时获得所有客流的列车分配结果,并根据模型结构特点设计拉格朗日松弛启发算法。对京沪高速铁路及相关路网进行模拟应用,取得较好效果。     

基于ROPES的CTCS-3级列控系统车载设备的建模

针对列控系统传统建模方法存在的缺点,在对CTCS-3级列控车载设备进行需求分析、系统分析和对象分析的基础上,引入嵌入式系统的快速面向对象开发过程(ROPES)的建模方法。利用该方法进行CTCS-3级列控系统车载设备的体系架构设计,建立了系统的详细模型。利用Rhapsody工具,将模型转换成基于实时框架技术可执行的代码,自动生成测试案例,对模型进行验证。测试结果表明,该建模方法有效降低了软件设计的复杂度,缩短了车载设备软件的开发周期。     

联锁软件的Petri网形式化定义

用Petri网对联锁系统中的核心部分－联锁机中的联锁软件进行表式化定义和分析，以减少联锁系统中的不确定性因素，降低联锁软件的复杂性，保证联锁软件定义的正确性，并对该定义进行了形式化验证。同时以进程建立过程作为事例，说明了用Petri我形式化定义联锁软件的具体过程，采用分层模型化技术对联锁软件中的各个变迁（模块）进行逐级分解和验证，最终得到经过验证的，足够详细的联锁软件模型，利用该模型能对系统的一些重要性能（如安全性和实时性）进行分析和改进。     

基于Timed-UML顺序图的RBC交接形式化建模与分析

在CTCS-3级列控系统中,采用RBC技术将线路划分成多个管辖区段。当列车行驶并跨越相邻RBC交界区域时,控制权将会移交至前方相邻RBC,整个过程称为RBC交接。在运行中,RBC交接过程能否实时安全可靠地执行,直接影响着列车的行车效率和乘客的生命安全。采用一种基于添加实时约束的UML顺序图与时间自动机结合的模型来建立RBC交接场景。以双车载电台的RBC切换策略出发,建立切换的Timed-UML顺序图模型,然后按照UML-TA转换规则,建立得到完整的时间自动机网络模型。并利用UPPAAL验证工具对RBC交接模型进行形式化建模及分析,对模型的死锁和功能实现做了验证,从而达到对CTCS-3级RBC子系统的实时性以及设计规范合理性的验证目的。     

MBD技术在列车控制器软件开发中的应用展望

近年来，轨道交通行业飞速发展，随着新车型项目的展开及既有车型的迭代升级，列车中各关键子系统的控制器产品功能需要不断地升级迭代和技术创新。基于模型的设计（MBD）作为一种日趋成熟的开发技术，具有图形化设计、早期仿真验证、代码自动生成、配套文档自动输出等优点，相对于既有的软件文本代码开发方式，MDB技术更加高效、灵活。通过分析列车控制器软件的开发现状，对MBD技术进行调研梳理，阐述说明其开发流程，总结其技术优势；对MBD技术可行性及技术难点进行分析，列举其在国内外工程中的应用情况；结合列车控制器功能的开发进行应用展望，并列举了可通过MBD技术的开发项点。     

两种铁路信号系统双机热备结构可靠性与安全性分析

双机热备系统已广泛应用于现代铁路信号系统中,国内外学者对其可靠性和安全性进行广泛而深入的研究,但在研究的过程中并没有区分不同的系统结构,鉴于此,分析传统的仅具有故障自检和同时具备自检与比较程序互检的两种不同的双机热备结构。综合考虑共因失效、在线诊断、多故障模式等因素,建立两种双机热备结构的同构马尔可夫模型并对其进行仿真,根据仿真结果对两种双机热备结构的可靠性、安全性进行分析比较。分析结果表明,带比较程序的双机热备结构具有更高的可靠性和安全性,更适合在铁路上推广应用。     

基于RM48的双机热备ATO设计

列车自动驾驶(ATO)是列车自动控制系统(ATC)的重要组成部分.本文根据全自动无人驾驶系统(FAO)中ATO的功能需求和RM48安全芯片的安全架构,提出了基于RM48的ATO双机热备结构设计方案.利用马尔科夫模型研究了双机热备ATO系统的可靠性,并且通过仿真工具分析了双机热备ATO和单机ATO的可靠性.仿真结果表明,双机热备ATO的可靠度比单机ATO具有明显的优势,完全可以满足全自动无人驾驶的可靠性需求.     

基于双总线的城市轨道交通列车网络主控设备冗余控制设计

以某在研的新型城市轨道交通车辆的列车控制与管理系统的设计研发工作为依托,从提高列车运行安全的角度出发,提出了在配置两种控制总线的列车上网络主控设备同时实现总线级和设备级热备冗余控制的设计思路,并在软件实现后进行了实验室模拟,验证了该设计在保证控制系统运行稳定性的同时,使热备冗余功能得到了优化。研究成果为未来轨道交通车辆的列车控制与管理系统设计提供了借鉴。     

高速铁路CTC分界口临时限速系统建模与验证

临时限速是高速铁路列控系统的重要组部分,CTC行车调度台分界口处的临时限迷信息交互频繁,对实时性的要求也更苛刻.为满足其实时性要求,采用时间自动机理论,结合分界口处临时限速相邻设备间的交互过程,分别建立各设备的时间自动机模型,通过时间自动机的积构建整个交互系统的网络模型,并利用UPPAAL验证工具对模型的功能和性能属性进行形式化验证.验证结果确认了交互过程中系统的安全性和受限活性.     

信号集中监测系统中电务段服务器子系统的设计研究

根据2010年颁布的铁路信号集中监测系统技术标准规定,电务段服务器子系统的功能及地位都得到了极大提升。故介绍一套基于广域网互联互通基础上的信号集中监测段服务器子系统的方案,阐述其系统结构、功能定义、热备方案以及软件信息流等具体技术问题的解决方案。     

CRH_3型动车组辅助供电系统可靠性研究

辅助供电系统可靠性对动车组的安全正常运行至关重要。为研究其可靠性,深入分析了CRH3型动车组辅助供电系统各组成结构及逻辑功能关系,建立了辅助供电系统可靠性框图模型。在此基础上,依据系统可靠性理论与武广高铁CRH3型动车组辅助供电系统故障统计数据,分析计算CRH3型动车组辅助供电系统各部件的故障率和可靠度,并结合最小路集不交化算法,计算评估了CRH3型动车组辅助供电系统的可靠性。为进一步提高系统可靠性,提出了在辅助供电系统关键设备配电网络中增加热备冗余支路的优化方案,计算结果验证了所提出方案的有效性。研究结果为CRH3型动车组辅助供电系统维护维修及可靠性优化提供依据。     

上海地铁B-TrunC(宽带集群通信)网络互联互通关键协议研究

[目的]上海地铁B-TrunC(宽带集群通信)网络采用了多线共享热备集群核心网架构,需接入多条线路不同厂商的基站及终端。为了实现网络互联互通,需对集群核心网与基站、终端的接口协议进行标准化设计。[方法]在B-TrunC标准基础上,对集群核心网与基站、终端的部分接口协议进行细化和补充。在核心网热备情况下,集群核心网与基站的接口需补充集群核心网主备倒换的流程协议,综合分析了两种既有核心网主备倒换实现方案的优缺点,提出了优化后的功能要求和流程协议;针对终端集群功能互联互通要求,提出了实现终端加载通话组、集中录音录像、多媒体消息功能互联互通的相关协议配置细化方案。[结果及结论]接口协议补充和细化后,接入两家厂商基站、终端的上海地铁B-TrunC网络热备集群核心网,实现了核心网倒换时所有基站、终端正常对应倒换,以及集群语音呼叫、实时短数据、多媒体消息功能互联互通,突破了B-TrunC网络化资源共享的关键技术瓶颈。     

联锁系统冗余结构设计方案及问题探讨

联锁系统是轨道交通系统中最基础的信号子系统，该系统对可靠性和安全性均有较高要求，为满足这些要求，需要对联锁系统的硬件和软件分别采取特殊的安全技术措施。从系统硬件结构、热备冗余功能和通信接口3个方面进行设计，并在设计过程中分别实施安全措施。在系统硬件结构设计中，采用组合式故障安全技术，从系统的内部独立性和外部独立性进行考虑；系统冗余功能设计中采用双机热备冗余功能，功能上重点考虑双机同步、双机切换、备系热备的逻辑进行设计；系统通信接口设计采用序列号、时间戳、CRC等技术保证通信数据的安全性。     

氢燃料电池动车组氢动力系统能量控制单元关键技术

以某型氢燃料电池动车组的氢燃料动力系统能量控制策略为例，系统地论述了氢燃料电池动力系统的能量管理策略和故障诊断策略，并通过系统联调对启停机、加减载及能量管理等控制功能进行验证。验证结果表明，所提控制方案可实现对氢燃料电池动力系统稳定可靠的控制，且实时性和跟随度较好，能够满足整车应用要求。     

基于层次分析法的全路客运车站等级评定研究

针对现有铁路客运车站等级评定中相关评价因素考虑不够全面,不能客观、合理地评定全路客运车站重要程度的难题,研究建立一种基于层次分析法的全路客运车站等级评定模型,综合考虑车站服务能力、资源条件、客流吸引力以及在路网中的地位等多方面因素;采集和整理全路所有客运车站的客运历史数据,使用R语言工具与数据库技术建立该模型,计算生成全路客运车站等级,并对等级评定结果进行分析。目前,由该模型计算生成的全路客运车站等级评定结果具有较强的实用性与参考价值,已在列车开行方案与运行图评估、铁路企业客票收入预算管理等多项业务中得到应用和验证。     

基于Timed RAISE的高速列车RBC切换协议形式化建模及验证

在CTCS-3(Chinese Train Control System Level 3)级列控系统中,RBC(Radio Block Center)切换是影响列车安全高效运行的重要环节,现阶段对RBC切换协议进行验证分析所使用的形式化方法还存在状态爆炸或描述性质单一等问题。基于Timed RAISE的形式化方法,结合域的模型,在对RBC切换流程分析的基础上,构建状态转移图,得到切换协议的形式化模型,使用等价和推断的推理规则对模型的正确性和实时性进行推理验证,得到的结果表明,RBC切换协议满足规范标准对正确性与实时性的要求,将验证结果与其他文献的结论进行比较分析,说明该方法具有通用性,对于推广其在列控系统场景验证中的应用有一定的实际意义。     

基于城市空间结构的轨道交通线网生成方法

为破解目前轨道交通线网规划方法主观随意性较大，形成的方案与城市发展和延伸方向不符，以及交通供给与需求难以在时空上很好匹配的问题，提出一种基于城市空间结构的城市轨道交通线网生成方法。首先，采用反距离修正的Infomap算法划分城市组团；其次，对线网数据进行前置数据处理，缩小模型的计算范围并推算得到线网密度、客流强度和线网规模3项关键参数；然后，构建线网生成模型，按照“组团间线网生成—组团内线网生成—线网整合与优化”的技术路线生成线网。依托某市实际数据构建算例，验证该线网生成方法的效果。结果表明：相比于该市的实际线网，前述方法得到的线网在布局上的延伸性更优，覆盖面积率提升68%，线网吸引范围内的公交站点数量更多，增加了639个，线网的全局可达性更高；增加的组团划分步骤，能够显著提升线网覆盖的中心城区面积率，生成线网的辐射力度和带动作用更强。