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

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

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

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

基于SSM-HAZOP的自主化ATP等级转换功能建模与验证

针对高速铁路列控系统安全完整性等级要求高、安全功能需求验证难等问题,考虑列控系统安全需求建模具有层次性、并发性等特点,以自主化ATP等级转换功能为例,综合运用安全状态机(SSM)建模理论,以及危险与可操作性分析方法 (HAZOP),提出一种基于SSMHAZOP的建模与自动验证方法。首先建立等级转换功能的SSM模型,然后基于HAZOP方法提取安全属性,最后利用SCADE DV工具自动验证等级转换的安全需求。结果表明,该方法能够满足列控系统等级转换安全需求建模与验证的要求,可应用于自主化ATP的安全验证。     

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

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

一种针对全自动运行系统的测试用例生成方法

针对全自动运行系统测试指定路径覆盖的测试需求,基于时间自动机建模理论提出满足指定路径覆盖和边覆盖的全自动运行系统测试用例自动生成算法。研究时间自动机建模理论,建立全自动运行系统的时间自动机模型;为表征全自动运行系统指定路径覆盖的测试需求,提出基于时间自动机模型的标记变量建模方法 ;结合Yggdrasil的测试用例生成机制,提出全自动运行系统测试用例生成方法,同时满足全自动运行系统测试的指定路径覆盖和边覆盖准则;以全自动运行系统的模式转换功能为例,建立时间自动机模型并生成测试用例。结果表明,测试用例100%覆盖测试人员指定的测试需求和时间自动机模型所有的边,能够满足全自动运行系统指定路径覆盖的测试要求。     

基于MSC与UPPAAL的区域控制器切换场景建模与验证

区域控制器(Zone Controller,ZC)边界切换场景是城市轨道交通列车控制系统的重要场景,切换过程中移交ZC、接管ZC和车载子系统之间要进行频繁的信息交互,因而对其安全性和实时性有更严苛的要求。根据ZC子系统特点,将MSC半形式化方法作为切入点,结合时间自动机理论,建立ZC切换场景的MSC模型和时间自动机网络模型,用于ZC切换场景功能和受限活性的安全验证。结果表明:ZC边界切换控制功能满足系统安全性和受限活性的规范要求。因此此种建模验证方法是可行的,可以将其应用于列控系统其他场景的建模与验证过程中。     

基于时间自动机的CBI道岔转换时间建模与验证

针对CBTC计算机联锁安全性十分重要的问题，介绍时间自动机理论，分析CBTC计算机联锁系统的结构和与传统联锁系统的区别，以CBTC联锁系统的道岔转换功能为例，采用UPPAAL建立了道岔转换模型，分析模型的安全需求。表明了在联锁系统开发过程中采用基于时间自动机建模与验证的方法的可行性和有效性。     

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

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

客运专线CTCS-3级列控系统无线闭塞中心的建模与验证

本文分析客运专线CTCS-3级列控系统中无线闭塞中心(RBC)子系统软件的功能和性能约束,在此基础上采用时间自动机理论进行RBC子系统形式化语义描述,建立TER-QSR时间自动机网络模型,并应用UPPAAL验证工具对RBC子系统进行仿真分析,验证RBC的安全性(Safety)和受限活性(Bounded Liveness),同时进行RBC切换时间的优化。     

基于时间自动机模型的安全计算机平台的形式化验证

众多工业控制领域要求计算机控制系统具有高可靠、高可用和高安全的运行基础,2乘2取2冗余结构的安全计算机平台是提高系统安全性、可靠性的一种重要解决方式。CBTC列控系统的安全计算机平台采用2乘2取2冗余结构,它是一个实时系统,控制过程需要考虑时间因素。本文分析CBTC系统安全计算机平台系统的组成结构,提取出系统的功能约束,采用基于时间自动机理论的建模验证工具UPPAAL建立系统的自动机网络模型,进行仿真分析,验证系统的功能性、实时性、安全性要求。     

基于钢垫梁的CRTSⅡ型板式无砟轨道支承层修复技术研究

针对高速铁路CRTSⅡ型板式无砟轨道支承层伤损,以影响运输效率最小化、作业效率最大化为原则,提出钢轨切割、轨道板移出、砂浆清理、钢垫梁临时支撑、伤损支承层修复、轨道板复位和砂浆层灌注的作业方案。并以关键工装钢垫梁为研究对象,进行承载能力静载试验和有限元数值分析,论证该技术方案的可行性。在钢垫梁临时支撑阶段,采用视频监控及动力学监测技术手段,实时监控线路状态,保障施工安全。应用实践表明:该技术能在天窗时间内完成CRTSⅡ型板式无砟轨道支承层伤损修复,有效改善线路高低不平顺,恢复无砟轨道结构稳定性。     

茂县隧道挤压性变形段锚杆作用效果分析

针对茂县隧道穿越活动断裂带及其影响区所遇到的挤压性变形问题,通过对1号斜井及左洞前期施工变形统计分析,以及现场锚杆施工存在的问题,针对性地提出锚杆施工工艺的改进措施,并开展长期跟踪监测。研究结果表明:锚杆工艺改进前,1号斜井和左洞收敛均值分别为689.2 mm和624.8 mm,且1号斜井变形不收敛,左洞收敛时间达6个月;锚杆工艺改进后,左、右洞水平收敛均值分别为320.4 mm和141.2 mm,相比左洞工艺调整前分别下降77.4%和40.6%,且收敛时间缩短至约4个月;按"孔腔通畅+非收缩浆液+可简单验证和不可逆转灌注满浆"的思路综合性改进锚杆施工工艺可显著提升锚杆质量,发挥其在抑制隧道挤压性变形中应有的作用。     

绵阳市近期轨道交通线网一体化衔接模式研究

为了充分发挥轨道交通的高效性、舒适性和快捷性,扩大轨道交通服务范围,从交通一体化发展策略角度,研究国内外如伦敦、东京、莫斯科、广州等城市的轨道交通一体化衔接模式。基于绵阳市近期轨道交通系统的建设规划,提出建立与绵阳市客运发展战略相适应的模式:构建"5大衔接分区、3大衔接系统"的交通一体化衔接系统。     

多跨地铁车站洞桩法施工及控制技术研究

以石家庄轨道交通3号线三教堂站多跨洞桩法施工为例,采用现场调研与数值模拟相结合的方法,研究了车站开挖过程中自身结构受力状态及对周围环境的影响规律,并提出适宜的控制技术。结果表明:采取措施后,地表沉降量在影响最大的两个阶段得到控制,同时管线累计沉降量减小,且车站主体结构受力状态得到较大改善,表明了控制技术的有效性。     

城市快速轨道交通敷设方式经济性与适应性研究

城市快速轨道交通是连接主城区与近郊城区的快速公交通道,线路长度长、站间距大。不同于主城区的轨道交通线路,其敷设方式选择对工程规模、投资控制、运营管理尤为重要。以成都轨道交通10号线二期工程为例,研究城市快速轨道交通线路的敷设方式。通过合理确定敷设原则、精细化的线位方案比选以及多专业协调设计,建议城市快速轨道交通线路尽可能多采用经济性好、建设速度快的高架敷设方式。     

基于极限分析有限元与强度折减法的边坡稳定性分析方法

采用极限分析有限元结合强度折减理论对边坡稳定性进行研究,定义无量纲参数P并将所得边坡安全系数作为判定边坡是否失稳的依据,将计算所得安全系数与已有文献结果进行比较验证,验证结果表明所采用方法能够更好地评估边坡稳定性。对不同参数影响下的边坡稳定性进行分析,讨论了摩擦角对边坡失稳破坏模式的影响。研究结果表明:所采用方法求得的安全系数上下限差值小于1%,可以用上下限的平均值来评估边坡安全系数;边坡坡脚、摩擦角和P对边坡稳定性均有很大的影响。     

成都轨道交通10号线的复合功能定位及其行车组织方案

介绍了成都轨道交通10号线各期工程的功能定位。一期工程为机场专线,线路向南、北延伸后为复合功能线,既是衔接中心城区与双流、新津片区的大运量级别市域快线,也是为机场客流服务的机场线。针对各期线路、客流的特点,提出了相应的行车组织方案,以保证设计方案的合理性和高效性。     

地铁转向架一系簧下盖螺栓断裂分析及改进措施

对某型地铁一系簧下盖螺栓断裂问题的原因进行分析,结合断裂螺栓理化分析、一系簧下盖螺栓线路工况载荷台架试验模拟,确定了钢弹簧调整垫摩擦阻力不足为故障直接原因。针对故障原因,进行了钢弹簧调整垫设计方案改进。基于台架试验,验证了改进方案的有效性。     

现代有轨电车车辆段站场总平面布置方法

从设计思路、影响因素和总平面布置结构型式三个关键环节对现代有轨电车车辆段站场总平面布置方法展开研究,分析了总平面布置中各专业系统的工作流程,以及车辆段选址、车辆段配属车数、车辆工艺和生产办公用房需求等影响因素对总平面布置的影响,对站场总平面布置结构型式和适应性进行了归纳和分析。提出了现代有轨电车配属车数估算方法,归纳总结了现代有轨电车站场总平面布置的工作流程和6种通用结构型式。针对现代有轨电车车辆段站场总平面布置的关键问题,提供了有效可行的解决方法。     

250km/h城际动车组低噪声设计技术

针对我国250 km/h城际动车组列车车内噪声控制问题,提出由问题导向式的被动噪声控制提升为低噪声正向设计,让车内声学指标变得可控。从声学技术规范、部件声学设计、整车声学仿真及优化、样车试验、减振降噪关键技术等方面着手,开展车内低噪声设计技术研究等方面工作。介绍了低噪声设计研究思路和声学设计参考标准,详细阐述了低噪声设计方法和试验方法。研究成果可为我国250 km/h城际动车组振动噪声控制提供依据,同时为动车组列车减振降噪提供参考。