基于微分动态逻辑的无线闭塞中心交接协议建模与验证

来源 :中国铁道科学 | 被引量 : 0次 | 上传用户:yys68738464
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
ETCS-2级列车运行控制系统呈现复杂的混成性.按照无线闭塞中心(RBC)交接协议的内容,建立RBC交接协议的UML图;基于微分动态逻辑理论,从混成系统角度对ETCS-2级列控系统规范中的RBC交接协议进行建模.建立的RBC交接协议模型包括列车子模型、移交子模型和接收子模型.根据模型的性质,构造微分不变式,运用证明工具KeYmaera验证模型的安全性和活性.结合专业知识对关键性的约束条件进行分析并将其反馈至模型,实现模型的精化.在模型验证过程中,发现了交接安全及交接效率的参数约束条件,由此参数约束条件可知
其他文献
根据现场长期实测数据分析,大秦铁路牵引供电系统具有负荷幅值变化大、过载系数高和陡变性的间歇性重负荷特性,牵引供电系统负荷的变化对变压器套管介质损耗因数的测量产生影
XML并发控制协议可用于保证多个用户同时访问XML文档时的事务隔离性。由于XML数据的半结构化特点和访问接口的特殊性,现有XML并发控制协议随着文件规模的增大、并发客户的增多,系统事务性能大幅下降。基于模型检测技术提出了一种新的乐观并发控制协议XOCC-MC。通过将XML文档对应的DTD文档转换为系统模型,将事务操作中的XPath转换为CTL公式,利用模型求值判断节点间是否存在A/D关系,进而根据
结合上海至南通铁路过江通道工程,针对设计构思的千米级跨度桥梁方案,进行主跨1 008 m斜拉桥和悬索桥力学性能研究。按照我国双线铁路标准布置荷载,考虑客货共用,进行桥梁静
通过武广客运专线某路桥过渡段的现场车检数据分析,对高速铁路路桥过渡段轮轨力随列军速度的变化规律进行研究。结果表明,动车通过路桥过渡段时轮轨垂向力明显增大,且当车速达30
针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法.引入了HCSP的假设条件,建立列控系统的行为模型;定义了HCSP到混合自动
针对青藏铁路气候的特点,运用试验和灰色关联分析方法,研究水灰比、养护温度和养护时间对桥梁压浆材料早期冻胀变形的影响规律及影响程度。试验研究表明:不同水灰比、不同养护
17单元板式无砟轨道设计技术的研究针对时速200~250km客货共线铁路、300~350km客运专线和高速铁路,开展了单元板式无砟轨道设计理论和设计方法的研究,包括:设计荷载和设计参数
根据已有试验结果,得到适用于铁路低配筋混凝土桥墩的荷载位移双折线模型。选取4类场地的320条实际地震记录,利用该双折线模型研究4类场地的强度折减系数谱值随桥墩屈服后刚
近些年,科研社交网站中的科技论文数量呈现出爆炸式增长的趋势,用户很难发现符合自己要求的科技论文,而科技论文推荐正是解决这个问题的有效方法之一。但是现有科技论文推荐方法大多专注于评分预测的准确性,忽视了推荐科技论文之间的排序问题,并且现有的科技论文推荐方法没有充分利用科研社交网站中的社会化信息。为此,提出了一种改进List-wise的科技论文推荐方法,系统地分析了科研社交网站中的好友关系,科技论文的
通过理论分析和试验,研究高强纤维片材(FRP)抗弯加固钢筋混凝土(RC)梁中FRP应变随构件变形及外加荷载的变化规律以及FRP的极限剥离应变。结果表明:FRP应变与RC梁的挠度成线性关系,