基于MSC与UPPAAL的列控系统等级转换场景形式化验证

等级转换是C3级列控系统的重要场景,是列控系统兼容性的集中体现,转换的成功与否直接关系到列车的运行安全和行车效率。因此,有必要对设计规范中所描述的转换过程进行形式化建模和验证,以保障系统的安全性和实时性。为保证设计规范与所建模型的一致性,采取消息顺序图(MSC)与时间自动机相结合的方式,建立等级转换场景中C2级向C3级转换过程的MSC模型,并将其转换为时间自动机模型。应用UPPAAL对模型的安全性和受限活性进行仿真验证,结果表明设计规范中所描述的转换过程是安全可靠的,可以满足C3级列控系统的兼容性和安全性要求。     

基于TRSL的RBC等级转换场景研究

无线闭塞中心等级转换场景作为中国列车运行控制系统主要场景之一,切换成功与否直接影响高速列车的安全和运行效率。通过对形式化验证方法的分析,采用基于定理证明的时间化工业软件工程规范语言的严格方法(Timed Rigorous Approach to Industrial Software Engineering Specification Language,TRSL),在对等级转换过程进行分析的基础上,设计交互信息图,构建状态迁移图,并结合域建模方法实现对该场景的TRSL描述,最后利用语言推理规则,结合系统特性,实现对切换正确性和实时性的双重验证,结果表明:该场景满足系统规范对功能性和实时性的要求,继而说明该方法的有效性、正确性和通用性,为我国列控系统的设计开发和验证提供一种新的途径和依据。     

基于时间自动机的自主化ATP等级转换功能建模与验证

自主化ATP(列车自动保护)系统在国产化ATP系统的基础上,增加了一些新的功能需求。针对自主化ATP系统安全关键功能的安全性和正确性保障的问题,以自主化ATP系统中典型的C2等级转换C3等级的等级转换功能为研究对象,采用时间自动机形式化地分析等级转换功能的安全性、活性和实时性。研究时间自动机的数学理论基础,分析自主化ATP系统等级转换功能的逻辑和与其他系统的数据交互;采用时间自动机建模方法,从ATP、RBC(无线闭塞中心)和应答器3个方面,建立C2等级转换C3等级的时间自动机模型;研究自主化ATP系统等级转换功能需要满足的安全性、活性和实时性要求,利用UPPAAL软件验证等级转换功能的系统性质。结果表明,自主化ATP系统C2等级转换C3等级功能满足期望的系统需求。     

CTCS-3级列控系统等级转换运营场景分析与研究

CTCS-3级列控系统是基于无线信息传输(GSM-R)的列车运行控制系统,目前有14个运营场景。针对其中的等级转换运营场景进行了初步分析,包括各种不同线路条件下等级转换应答器组的布置,等级转换点内方不同进路条件下的等级转换情况,以及降级情况下的等级转换处理等内容。     

基于场景法的列控系统等级转换功能测试用例设计

为了改善当前列控系统等级转换功能测试用例覆盖不全面的问题,以CTCS-2级转CTCS-3级功能为研究对象,采用场景法分析转换逻辑,设计测试用例。首先,分析CTCS-2级转CTCS-3级的功能逻辑;然后,介绍场景法设计测试用例的过程及基本流和备选流划分原则;最后,采用场景法对CTCS-2级转CTCS-3级过程中的基本流和备选流进行划分,确定基本流和备选流有向图,设计测试用例。结果表明,该方法设计的测试用例能够提高列控系统功能性和安全性测试的完备性,从而保障列控系统产品的质量。     

Timed RAISE方法在列控系统等级转换场景中的应用研究

高速铁路列车运行控制系统是一个复杂的实时性系统,结合其实际特点,将域方法作为系统描述的切入。通过对模型检验和定理证明两种验证方法的分析比较,提出使用基于定理证明的时间化工业软件工程的严格方法Timed RAISE形式化方法对等级转换(CTCS-2级至CTCS-3级)场景进行描述,并对其场景交互一致性和实时性进行验证,结果表明该场景不会出现场景交互一致性错误,也不会违反时间的约束。     

沈阳枢纽等级转换方案设计简述

以沈阳枢纽为例,介绍枢纽中等级转换方案设计时需要兼顾线路状态、站场因素、运输组织、过渡修改、软件换装的影响、工程投资等制约或影响枢纽等级转换设计的因素,同时充分利用报文特性、车载特性,使得既能满足功能需求,又减少工程投资和软件过渡。     

CTCS-2至CTCS-3等级转换的研究及仿真

分析CTCS-2级转换至CTCS-3级的具体流程以及转换过程中的车地信息交互。以西南交通大学CTCS-3级列控系统仿真平台为研究对象,针对该系统CTCS-2级至CTCS-3级等级转换的功能空缺,在车载子系统中增加等级转换控制模块,完善地面子系统相关功能,并对CTCS-2级至CTCS-3级的等级转换功能进行仿真测试。结果表明,该平台能够正确地完成CTCS-2级至CTCS-3级的等级转换,实现等级转换过程中超速防护功能及司机提示功能,并对等级转换过程中车地仿真消息进行实时记录和显示。     

基于在线一致性测试理论的CBTC车载ATO功能测试研究

自动列车驾驶系统(ATO)是CBTC系统的重要组成部分,验证测试其控制功能逻辑的正确性和安全性至关重要。介绍了ATO控制原理和功能,分析了CBTC中典型的两车追踪控制运行场景控制流程,得到了该场景下的列车运行安全需求。结合时间自动机理论,建立了包含列车动力学、车载ATO、ZC以及时钟控制器的两车追踪场景时间自动机网络模型,验证了模型中安全需求的正确性;基于一致性测试理论,定义了被测车载ATO软件与测试环境的可观测输入/输出接口,利用UPPAAL-TRON工具设计了被测车载ATO软件的一致性测试框架,并进行了一致性测试分析。在此基础上,采用变异测试,针对典型的车载ATO软件功能实现错误(错误的安全距离、静态限速、功能逻辑以及命令丢失等)进行了安全性验证。结论表明:该在线一致性测试方法能够及时发现车载ATO软件行为与规范模型的不一致,有效提升了车载ATO功能测试的检错能力。     

CTCS-3至CTCS-2等级转换应答器组布置

CTCS-3至CTCS-2级列控系统等级转换应答器布置非常重要。等级转换应答器布置不当,会引起列车紧急制动。通过对CTCS-3级列控系统应答器应用原则研究,介绍CTCS-3至CTCS-2等级转换应答器组布置原则,并详细分析特殊场景下引起列车紧急制动的原因。最后结合特殊场景,提出优化等级转换应答器布置的方法。     

等级转换应答器组布置原则探讨

为了实现列车运行过程中不停车自动实施CTCS-3/CTCS-2等级转换,在特殊线路情况下需要更加明确等级转换应答器组布置原则。通过对CTCS-3总体技术方案研究,介绍等级转换的基本流程及等级转换应答器组布置的基本原则,并详细分析在特殊线路情况下等级转换应答器组布置应避免的情况,最后指出等级转换应答器组布置原则在工程项目中需要进一步研究完善。     

关于动车组车载设备在非等级转换点处自动转换的原因分析

针对动车组ATP、LKJ设备运行途中突然自动转换的问题,进行了深入调查分析。通过分析,查找出故障原因,采取针对性措施,减少对铁路运营造成的影响。     

CTCS-2/CTCS-3级列控系统等级转换基本原理与实现

CTCS-2/CTCS-3及列控系统等级转换是CTCS的关键课题之一,通过对CTCS-3级列控系统总体技术方案研究,介绍了CTCS-2/CTCS-3等级转换原理,并详细分析了CTCS-2/CTCS-3等级转换过程中地面应答器设备、RBC设备以及车载ATP设备信息交互过程。最后结合工程应用需求,提出等级转换点设计需要进一步研究讨论的问题。     

合福高铁引入合肥枢纽列控系统等级转换方案探讨

通过对枢纽内各线间相互衔接关系的梳理,并结合CTCS-2与CTCS-3级列控系统等级转换原则,提出动车组在合肥西合福场与宁西场跨合福线和合武绕行线运行的3种等级转换方案。并且对3种等级转换方案进行深入细致的分析探讨,总结出各方案的优缺点。为将来新建高速线路引入枢纽后动车组跨线运行时不同等级列控系统之间等级转换提供几种解决方案及思路。     

C2/C3等级转换设置方案优化探讨

根据列车运行控制系统C2/C3等级转换的相关规范、RBC和ATP设备C2/C3级间转换时的处理过程,对工程实施过程中存在的C2/C3级间转换设置问题进行了分析研究,并提出相应的优化措施。     

CTCS-2级列控车载设备层次化组合测试方法

对列控车载设备开展组合测试,可有效提高设备的安全性。针对现有组合测试方法未充分考虑车载设备测试过程中输入的时序性、设备状态等影响软件安全的各种因素组合的问题,提出一种车载设备层次化组合测试方法。首先,划分CTCS-2级车载设备测试过程中各种影响因素的组合层次,设置层次化覆盖强度。其次,提出了车载设备层次化组合覆盖准则,给出形式化定义,构建层次化组合测试模型。然后,提出一种两阶段层次化组合测试用例生成方法,高效精简构造层次化组合测试集。最后,以CTCS-2/0等级转换测试为例对方法进行验证。结果表明,在保证各种影响因素组合覆盖的前提下,相对于现有方法,在覆盖强度t={2,2,2}时,采用本方法的测试成本可降低23.53%,有效提高测试的针对性,验证了方法的有效性。     

高速铁路枢纽站信号联锁分界及列控等级转换设计方案研究

随着国家高速铁路网络“八纵八横”战略的逐步推进实施,既有高铁枢纽站因新线引入而增加车场的情况越来越普遍。在一站多场、多场间短联络线跨场通过等列车进路中,联锁、列控区域的合理划分成为信号系统工程设计的重点和难点。合理的联锁分界和列控等级转换方案,可为后期建设、运营维护节约大量人力、物力成本。以某车站为例,总结新线引入既有高铁枢纽信号系统的技术需求;研究高速铁路枢纽复杂联络线跨场区域内,联锁区域分界、列控等级转换的实施方案。该方案可应用于高速铁路枢纽工程设计领域,为铁路信号系统设计和实施提供合理依据,同时为解决复杂枢纽联锁分界和列控等级转换问题提供参考。     

高速铁路CTCS-3级列控系统等级转换工程应用研究

高速铁路CTCS-3列车运行控制系统等级转换是工程设计及系统集成的重要内容之一.列控系统等级转换在地面系统中设置等级转换点,由车载设备完成等级转换.等级转换位置受线路长度、转换点处速度、临时限速、分相区设置等多种因素限制,在工程应用中,地面系统需结合车载设备的控制逻辑进行综合分析.如果等级转换预告点或执行点设置不当,可...     

基于Testcase Designer的列车运行控制系统测试方法的研究

针对CTCS-3级列控系统的需求规范,结合欧洲列车运行控制系统（ETCS）的测试经验,研究基于Testcase Designer的CTCS-3级列控系统自动测试方法。Testcase Designer主要用于将测试案例模块化,通过优化编写流程,生成符合测试平台需求的测试序列,为测试项目的执行提供必要的关键数据点。同时,Testcase Designer可供存储、导出及发布。其测试案例中的关键输入输出接口（如BTM、TIU、RTM等）配置信息均已通过配置文件形式实现。以列控系统无线闭塞中心（RBC）切换场景为例,采用Testcase Designer编写该场景的测试案例。研究结果表明:Testcase Designer实现了功能特征、参考需求、测试步骤等元素的集成,编写的测试案例是合理的。     

基于UPPAAL的FAO系统典型运营场景建模与验证

全自动驾驶系统FAO(Fully Automatic Operation)具有安全、可靠、高效的特点,成为未来城市轨道智能交通系统的主要发展方向。FAO系统典型运营场景是1个实时的过程,为发现其逻辑的错误、功能和性能的缺陷,需要在系统设计前,针对系统需求规范中典型运营场景的实现流程进行形式化分析。本文分析FAO典型运营场景保护区的实现流程,在系统需求规范中提取其功能与性能的需求,采用基于时间自动机理论的UPPAAL构建时间自动机网络模型,进行仿真分析,并验证其功能属性、性能属性与安全属性。通过反例分析、模型修正,增强对FAO系统的理解,减少设计故障,提高安全性,为系统设计与实现打下良好的基础。