共查询到20条相似文献,搜索用时 187 毫秒
1.
针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法。引入了HCSP的假设条件,建立列控系统的行为模型;定义了HCSP到混合自动机(HA)的转换规则,将HCSP模型转换成HA模型;利用模型检验工具PHAVer对HA模型进行自动验证。以高速铁路列控系统典型的行车许可运营场景为例,建立区间闭塞分区行车许可场景的HCSP模型;根据转换规则将行车许可场景的HCSP模型转换成HA模型;用PHAVer验证了所建立的区间闭塞分区行车许可场景模型的正确性,从而证明了基于HCSP的高速铁路列控系统建模及验证方法的有效性。 相似文献
2.
基于MSC与UPPAAL的列控系统等级转换场景形式化验证 总被引:3,自引:3,他引:0
等级转换是C3级列控系统的重要场景,是列控系统兼容性的集中体现,转换的成功与否直接关系到列车的运行安全和行车效率。因此,有必要对设计规范中所描述的转换过程进行形式化建模和验证,以保障系统的安全性和实时性。为保证设计规范与所建模型的一致性,采取消息顺序图(MSC)与时间自动机相结合的方式,建立等级转换场景中C2级向C3级转换过程的MSC模型,并将其转换为时间自动机模型。应用UPPAAL对模型的安全性和受限活性进行仿真验证,结果表明设计规范中所描述的转换过程是安全可靠的,可以满足C3级列控系统的兼容性和安全性要求。 相似文献
3.
与传统列控系统相比,全自动无人驾驶运营场景更加复杂多变,潜在的危险及致因具有更强的隐蔽性和复杂性,给运营安全带来了新的挑战。针对以上问题,提出一种STAMP(Systems-Theoretic Accident Model and Process)与模型检验相结合的复杂运营场景安全验证方法。首先,基于STAMP理论构建运营场景分层控制结构模型,辨识潜在的不安全控制行为、分析危险致因和安全约束;其次,定义分层控制结构模型与安全状态机模型间的基本转换规则,基于分层控制结构模型、安全约束和转换规则,构建运营场景安全状态机模型;最后,针对提取的安全约束,利用数据流图建立安全属性验证模型,结合模型检验技术,对运营场景安全状态机模型进行形式化验证。以全自动无人驾驶运营场景中列车自动进站停车为例,对方法进行验证分析。结果表明,当STAMP理论提取的安全约束通过了场景安全状态机模型的验证时,表示在该场景中对应的不安全控制行为没有发生且不导致相应危险。该方法结合系统安全分析与形式化建模验证的优势,降低了运营场景建模的难度,构建的运营场景形式化模型满足系统安全约束,可以作为全自动无人驾驶系统安全设计和安全... 相似文献
4.
为满足列控系统交互性、混合性、反应性和并发性的复杂特性,从研究分布式复杂系统的多智能体方法出发,利用UML2.0扩展的AUML统一建模语言,提出一种列控系统运营场景多智能体建模方法。该方法采用基于Agent的AUML,以多智能体建模理论为基础,从系统功能需求、抽象Agent定义、Agent信息交互和Agent内部设计四个步骤对列控系统运营场景进行模型构建。最后以RBC切换场景为例,建立RBC切换场景的多智能体模型,结合模型,利用仿真工具进行仿真,得到满足列控系统复杂特性的仿真结果。结果表明:该建模仿真方法符合列控系统交互性、混合性、反应性和并发性,为列控系统研究奠定重要的仿真环境基础。 相似文献
5.
针对高铁列控系统的并发性、混成性、交互性等特点,基于列控系统技术规范,结合Multi-Agent理论、Prometheus建模方法以及仿真技术,提出基于Multi-Agent的高铁列控系统复杂运营场景建模与仿真方法。最后,以CTCS-3级列控系统的RBC切换场景为例,构建基于Multi-Agent的RBC切换场景模型,并利用Multi-Agent仿真工具对模型进行仿真。仿真结果表明,该方法能够满足列控系统并发、混成、交互的复杂特性,可为列控系统复杂运营场景建模仿真与安全分析提供技术支撑。 相似文献
6.
高速铁路列车运行控制系统是保证列车安全、高效运行的核心设备,如何验证系统功能的正确性从而提高系统的安全性是至关重要的。引入了一种基于进程演算的方法—混合通信顺序进程(HCSP ,Hybrid Communication Sequential Process),利用该方法对列控系统进行了形式化描述,并针对典型的场景—注册与启动场景进行了HCSP建模,通过引入转换规则,进行了相应模型转换,应用模型检验工具UPPAAL进行了仿真和功能验证,验证结论表明了场景模型功能的正确性以及方法的可行性。 相似文献
7.
区域控制器(Zone Controller,ZC)边界切换场景是城市轨道交通列车控制系统的重要场景,切换过程中移交ZC、接管ZC和车载子系统之间要进行频繁的信息交互,因而对其安全性和实时性有更严苛的要求。根据ZC子系统特点,将MSC半形式化方法作为切入点,结合时间自动机理论,建立ZC切换场景的MSC模型和时间自动机网络模型,用于ZC切换场景功能和受限活性的安全验证。结果表明:ZC边界切换控制功能满足系统安全性和受限活性的规范要求。因此此种建模验证方法是可行的,可以将其应用于列控系统其他场景的建模与验证过程中。 相似文献
8.
《铁道标准设计通讯》2018,(12)
针对在列控系统建模和形式化分析领域UML模型难以直接描述系统安全特性的问题,提出一种利用UML支持的底层扩展机制对HUML进行面向列控系统安全特性的扩展方法。该方法给出列控系统安全特性需求,通过在HUML元模型中增加安全特性包,对安全特性元素进行定义,创建安全相关概要文件,并在建模软件中得到实现,最后介绍该方法在CTCS-3级列控车载设备故障方面应用的一个实例。新的建模方法丰富了列控系统HUML模型的表达能力和应用范围,使得列控系统安全特性能够直接被描述,从而将安全分析的起点提前至系统建模阶段,为列控系统建模和形式化分析提供一条新的思路和途径。 相似文献
9.
CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节。然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验证显得十分必要。本文提出CTCS-3级列控系统规范建模与形式化验证方法,此方法的特点是能够在系统规范、模型、验证工具以及验证结果之间建立一条跟踪链,从而始终保证系统规范、模型及程序代码之间的一致性。结合笔者运用此方法对CTCS-3级列控系统规范建模与形式化验证的实践,证明这种方法是可行的、高效的。 相似文献
10.
11.
12.
列车控制网络是面向控制的一种连接车载设备的网络通信系统,是分布式列车控制系统的重要组成部分,它能够通过信息的实时交互来实现对列车各种车载设备的通信、管理与控制等.通信协议是网络运行的最基本的保障,协议实现情况的好坏对于网络以及列车的正常运行都有重要的意义.本文对CRH2型车通信网络协议实现情况的分析方法进行了研究,并且设计了协议实现情况的分析工具,分析内容包括协议报文封装的分析,协议工作流程的分析,不同应用报文封装的分析,不同应用工作流程的分析等. 相似文献
13.
14.
ARCNET网络系统实时性能分析与研究 总被引:2,自引:0,他引:2
列车控制网络在列车控制系统中起着非常重要的作用,其实时性能直接影响到列车的安全可靠运行。对其实时性能进行分析评价可以优化设计列车控制网络的应用层,合理配置网络,优化网络性能,从而保证列车的安全可靠运行。本文介绍ARCNET列车控制网络的数据帧类型,数据通信机制和自动重构过程等,并对ARCNET网络通信延迟时间参数进行分析,建立ARCNET网络数据通信延迟时间模型、分析其网络实时性,并提出改进网络实时性的方法。最后在搭建的网络控制系统中,对实验测试结果和模型计算结果进行比较,验证模型的正确性。并利用分析结果以及建立的通信延迟时间数学模型,计算开发基于ARCNET轻轨列车网络控制系统的轮询周期,为系统应用层设计提供依据。 相似文献
15.
16.
17.
18.
19.
中国高速铁路列车控制系统(CTCS)包括地面列控系统和车载列控设备两部分。轨道电路是地面列控系统的基础设备。为保证列车控制系统的正常工作,轨道电路的布置既要满足地面列控系统的要求,同时也必须符合车载列控设备的技术条件。一般情况下,相邻轨道电路应设置不同载频。但在一些既有复杂枢纽,无法避免出现相邻轨道电路同基准载频的情形。在这种情况下,如果设计布置不当,会引起列控车载设备产生非正常制动。采用从列控车载设备逻辑功能角度对地面轨道电路的布置应用场景进行分析的研究方法,阐述相邻轨道电路同基准载频布置对列控车载设备的影响。提出的方案能够解决在无法避免出现相邻轨道电路同基准载频的情况下,合理布置轨道电路载频,保证列车的行车安全。 相似文献
20.
提出高速列车安全运行电磁控制系统(简称电磁安全控制系统)的设计方案。电磁安全控制系统采用主动控制方式,通过对现场采集的数据信息进行解析,获得轮对间受力情况,经核心运算输出控制信息,控制执行机构动作电磁系统,使两轮对间受力趋于平衡,实现对列车运行状况的实时调整和危险情况下的自动控制。最后,从系统的实现功能入手,对其进行动态模拟,并对所得数据进行分析、对比,完成对系统性能的试验论证。 相似文献