【摘 要】
：
车站联锁系统是一种典型的基于数据驱动的安全苛求系统,开发过程中需要对系统行为进行验证并需确认数据的正确性.为此,通过分析联锁系统的设计规范,基于RODIN平台并使用Event-B语言,辅助使用UML(unified modeling language)图工具快速建立系统的初始模型,以自动生成模型文件并描述出各系统属性与事件流程;基于精化策略分层建模,对各层模型的证明义务进行定理证明,验证了系统的各项属性,得出可靠的通用功能模型;基于实例车站,对模型的公理进行了验证,同时实现了对联锁数据的确认;通过形式化验
【机 构】
：
西南交通大学信息科学与技术学院,西南交通大学系统可信性自动验证国家地方联合工程实验室,西南交通大学唐山研究生院,北京和利时系统工程有限公司
【基金项目】
：
国家自然科学基金(71502146,61673320),中央高校基本科研业务费专项资金(2682017ZT12)。
论文部分内容阅读
车站联锁系统是一种典型的基于数据驱动的安全苛求系统,开发过程中需要对系统行为进行验证并需确认数据的正确性.为此,通过分析联锁系统的设计规范,基于RODIN平台并使用Event-B语言,辅助使用UML(unified modeling language)图工具快速建立系统的初始模型,以自动生成模型文件并描述出各系统属性与事件流程;基于精化策略分层建模,对各层模型的证明义务进行定理证明,验证了系统的各项属性,得出可靠的通用功能模型;基于实例车站,对模型的公理进行了验证,同时实现了对联锁数据的确认;通过形式化验
其他文献
互联网的安全形势日益严重,CSRF漏洞是最严重的Web漏洞之一,如何检测CSRF攻击成为业内热点.目前的CSRF检测技术主要通过验证字段例如Form表单字段、验证Same Origin等传统方
17-4PH不锈钢在经过固溶和时效处理时,通过马氏体相变和时效作用对材料进行强化。基于此,文章研究了不同时效热处理温度对17-4PH不锈钢金相组织及硬度的影响规律。研究结果表
针对隧道锚承载能力评价合理的解析计算公式缺乏、模型试验测试方法耗时费力、数值模拟可靠性不佳的问题,提出了一种人工智能化隧道锚承载能力预测方法.从隧道锚受力传力过程出发,分析了影响承载能力的因子,确定了承载能力评价指标体系;基于最小二乘支持向量机(least squares support vector machines,LSSVM)强大的学习预测能力和粒子群优化(particle swarm optimization,PSO)算法良好的优化效果,建立了承载能力非线性映射PSO-LSSVM模型;将收集到的1
为改善平钢板剪力墙受剪易屈曲及面外刚度小的问题,提出侧边加劲半圆形波纹钢板墙.基于两边连接侧边加劲半圆形波纹钢板墙的力学特点给出其简化力学模型,推导了弹性初始刚度及承载力公式,并给出弹性屈曲临界荷载计算公式;采用有限元软件ABAQUS对22个单层侧边加劲半圆形波纹钢板墙进行了弹性屈曲分析及非线性推覆分析,验证了理论公式的有效性;研究了各设计参数对侧边加劲半圆形波纹钢板墙屈曲性能和破坏模式的影响.研究结果表明:侧边加劲半圆形波纹钢板墙的弹性屈曲临界荷载较平钢板墙有显著提高;为保证侧边加劲半圆形波纹钢板墙发生
为了研究钢轨磨耗和疲劳裂纹萌生寿命与钢轨硬度的关系,基于Archard磨耗模型和临界平面法疲劳裂纹萌生预测模型,结合磨耗和型面变化分段迭代和疲劳损伤累积,提出了钢轨疲劳裂纹萌生和磨耗共存预测方法;对4种不同硬度钢轨的磨耗发展、疲劳损伤累积以及疲劳裂纹萌生寿命进行研究.结果表明:该方法预测的裂纹萌生寿命与现场观测结果有较好的吻合性;高硬度钢轨可以降低磨耗、延长疲劳裂纹萌生寿命,适合在小半径曲线上应用;4种硬度的钢轨中,钢轨硬度每提高10 HBW,平均磨耗发展率将降低约3%~6%,疲劳裂纹萌生寿命延长约9%~
针对莫喀(莫斯科—喀山)高速铁路季节性冻土区路基冻胀病害防治问题,提出了铺设保温板垫层的新型桩板结构路基.通过对聚苯乙烯泡沫塑料板(EPS)、聚氨酯板(PU)和挤塑聚苯乙烯泡沫塑料板(XPS)3种保温材料性能的对比分析,发现新型桩板结构路基中的保温板可采用在保温隔热、隔水防渗和抗压性能方面表现良好的XPS保温板.通过建立热弹塑性冻胀计算模型,研究了冻胀力作用下保温板铺设范围、厚度、路基填高和外界温度对新型桩板结构路基受力变形的影响.结果表明:当保温板铺设范围延伸到线路两端的信号线槽处时,可以更好地阻滞外界
基于交通视频监控图像的天气识别已经成为智能交通系统中重要的研究课题.虽然卷积神经网络(convolutional neural network,CNN)在图像识别技术获得了巨大的发展,但是针对复杂交通场景的天气识别问题,现有的模型在特征表达方面仍然面临着巨大的挑战.为了提取丰富的语义特征,提出了基于联合投票机制的深度神经网络(deep neural network,DNN)模型.所提出的模型包括两个核心模块:基于通道和空间注意力机制的二阶特征模块和基于复合特征结果联合投票机制的分类模块,用以提取不同天气图
为研究固定辙叉结构不平顺对列车过岔动力特性的影响,基于岔区轮轨系统动力学及轮轨接触关系理论,以12号提速道岔固定辙叉为例,分别建立了翼轨不同加高设计方案下的辙叉模型以及CRH2型车车辆模型,在此基础上,深入分析了翼轨加高设计对列车过岔动力特性、过岔速度以及行车平稳性的影响规律.结果表明:列车过岔时,随着翼轨向外弯折,其轮轨接触区域开始外移,并由此造成辙叉区轮对质心垂向位置的降低;通过设置合理的翼轨加高值,可有效降低辙叉区轨道的竖向结构不平顺,进而抑制轮对质心垂向位置的降低,提高列车过岔的平稳性及旅客乘车舒
为探明我国某地铁线路弹性短轨枕轨道曲线钢轨短波长波磨萌生原因,采用现场试验和数值仿真方法对其开展了研究.首先,通过现场试验确定钢轨波磨波长与轨道动态特性对应关系;其次,利用车辆-轨道耦合动力学模型计算轮轨接触参量,通过力锤敲击法获得现场轨道导纳特性;最后,基于轮轨接触参量和轨道导纳结果,建立钢轨波磨频域线性分析的数值模型,模拟弹性短轨枕轨道频域下曲线钢轨磨损率特征,分析了弹性短轨枕轨道萌生特定波长波磨原因.研究结果表明:地铁弹性短轨枕轨道钢轨波磨主要出现在半径小于等于800 m曲线段,低轨波磨程度更为显著
针对在非视距(non-line-of-sight,NLOS)环境中传统最优化定位算法抗NLOS误差能力较弱、且需要一个较准确的初始估计位置以确保算法收敛这一问题,提出一种应用在双基站场景下的基于几何约束及迭代的定位算法.通过引入最大散射半径作为几何约束条件,以线性迭代方式进行一维全局搜索,并采用最小二乘算法获得移动台(mobile station,MS)初始估计位置,然后利用设定的阈值门限对各初始位置点进行筛选,最后通过加权平均获得MS的最终估计位置.仿真结果表明:当散射半径为200 m时,本文算法的定位