基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法

针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法。引入了HCSP的假设条件,建立列控系统的行为模型;定义了HCSP到混合自动机(HA)的转换规则,将HCSP模型转换成HA模型;利用模型检验工具PHAVer对HA模型进行自动验证。以高速铁路列控系统典型的行车许可运营场景为例,建立区间闭塞分区行车许可场景的HCSP模型;根据转换规则将行车许可场景的HCSP模型转换成HA模型;用PHAVer验证了所建立的区间闭塞分区行车许可场景模型的正确性,从而证明了基于HCSP的高速铁路列控系统建模及验证方法的有效性。     

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

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

基于STAMP与模型检验的全自动无人驾驶复杂运营场景安全验证方法

与传统列控系统相比,全自动无人驾驶运营场景更加复杂多变,潜在的危险及致因具有更强的隐蔽性和复杂性,给运营安全带来了新的挑战。针对以上问题,提出一种STAMP(Systems-Theoretic Accident Model and Process)与模型检验相结合的复杂运营场景安全验证方法。首先,基于STAMP理论构建运营场景分层控制结构模型,辨识潜在的不安全控制行为、分析危险致因和安全约束;其次,定义分层控制结构模型与安全状态机模型间的基本转换规则,基于分层控制结构模型、安全约束和转换规则,构建运营场景安全状态机模型;最后,针对提取的安全约束,利用数据流图建立安全属性验证模型,结合模型检验技术,对运营场景安全状态机模型进行形式化验证。以全自动无人驾驶运营场景中列车自动进站停车为例,对方法进行验证分析。结果表明,当STAMP理论提取的安全约束通过了场景安全状态机模型的验证时,表示在该场景中对应的不安全控制行为没有发生且不导致相应危险。该方法结合系统安全分析与形式化建模验证的优势,降低了运营场景建模的难度,构建的运营场景形式化模型满足系统安全约束,可以作为全自动无人驾驶系统安全设计和安全...     

基于Multi-Agent的列控系统复杂运营场景建模与仿真方法研究

针对高铁列控系统的并发性、混成性、交互性等特点,基于列控系统技术规范,结合Multi-Agent理论、Prometheus建模方法以及仿真技术,提出基于Multi-Agent的高铁列控系统复杂运营场景建模与仿真方法。最后,以CTCS-3级列控系统的RBC切换场景为例,构建基于Multi-Agent的RBC切换场景模型,并利用Multi-Agent仿真工具对模型进行仿真。仿真结果表明,该方法能够满足列控系统并发、混成、交互的复杂特性,可为列控系统复杂运营场景建模仿真与安全分析提供技术支撑。     

基于AUML的列控系统运营场景多智能体建模仿真研究

为满足列控系统交互性、混合性、反应性和并发性的复杂特性,从研究分布式复杂系统的多智能体方法出发,利用UML2.0扩展的AUML统一建模语言,提出一种列控系统运营场景多智能体建模方法。该方法采用基于Agent的AUML,以多智能体建模理论为基础,从系统功能需求、抽象Agent定义、Agent信息交互和Agent内部设计四个步骤对列控系统运营场景进行模型构建。最后以RBC切换场景为例,建立RBC切换场景的多智能体模型,结合模型,利用仿真工具进行仿真,得到满足列控系统复杂特性的仿真结果。结果表明:该建模仿真方法符合列控系统交互性、混合性、反应性和并发性,为列控系统研究奠定重要的仿真环境基础。     

基于HCSP的列控系统安全性建模与验证分析

高速铁路列车运行控制系统是保证列车安全、高效运行的核心设备，如何验证系统功能的正确性从而提高系统的安全性是至关重要的。引入了一种基于进程演算的方法—混合通信顺序进程（HCSP ，Hybrid Communication Sequential Process），利用该方法对列控系统进行了形式化描述，并针对典型的场景—注册与启动场景进行了HCSP建模，通过引入转换规则，进行了相应模型转换，应用模型检验工具UPPAAL进行了仿真和功能验证，验证结论表明了场景模型功能的正确性以及方法的可行性。     

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

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

基于HUML扩展机制描述列控系统安全特性的研究

针对在列控系统建模和形式化分析领域UML模型难以直接描述系统安全特性的问题,提出一种利用UML支持的底层扩展机制对HUML进行面向列控系统安全特性的扩展方法。该方法给出列控系统安全特性需求,通过在HUML元模型中增加安全特性包,对安全特性元素进行定义,创建安全相关概要文件,并在建模软件中得到实现,最后介绍该方法在CTCS-3级列控车载设备故障方面应用的一个实例。新的建模方法丰富了列控系统HUML模型的表达能力和应用范围,使得列控系统安全特性能够直接被描述,从而将安全分析的起点提前至系统建模阶段,为列控系统建模和形式化分析提供一条新的思路和途径。     

CTCS-3级列控系统规范的建模与形式化验证方法研究

CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节。然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验证显得十分必要。本文提出CTCS-3级列控系统规范建模与形式化验证方法,此方法的特点是能够在系统规范、模型、验证工具以及验证结果之间建立一条跟踪链,从而始终保证系统规范、模型及程序代码之间的一致性。结合笔者运用此方法对CTCS-3级列控系统规范建模与形式化验证的实践,证明这种方法是可行的、高效的。     

基于UML的CTCS-3级列控系统运营场景分析方法研究及应用

CTCS-3级列控系统是典型的安全苛求系统,而对于安全苛求系统来说,系统需求规范中的安全隐患是最致命的。CTCS-3级列控系统的需求规范由14个运营场景来描述,因而以运营场景为单位,对规范进行分析与研究是合理的,并且是必要的。以UML和CSP为基础,提出一套适用于CTCS-3级列控系统运营场景的分析和验证方法,并以＂RBC切换＂场景为例,运用该方法分析了其活性、死锁、活锁、确定性和部分安全性。     

基于多Agent的列车分布式智能控制研究

有效的列车控制是铁路运输安全的重要保障,针对列车在物理上的分布特性及任务的多样性,提出了一种基于多Agent的分布式列车智能控制系统的体系结构,详细讨论了其各部分的组成及功能,给出了多Agent之间的通信方法及多Agent之间的协同机制。最后给出了列车速度控制的多Agent系统的协同控制过程。通过将多Agent引入列车控制系统中,可以改善控制系统各组成部分的协作能力和主动性、提高整个列车控制系统的能力。     

CRH2型动车通信网络协议分析系统的设计与实现

列车控制网络是面向控制的一种连接车载设备的网络通信系统,是分布式列车控制系统的重要组成部分,它能够通过信息的实时交互来实现对列车各种车载设备的通信、管理与控制等.通信协议是网络运行的最基本的保障,协议实现情况的好坏对于网络以及列车的正常运行都有重要的意义.本文对CRH2型车通信网络协议实现情况的分析方法进行了研究,并且设计了协议实现情况的分析工具,分析内容包括协议报文封装的分析,协议工作流程的分析,不同应用报文封装的分析,不同应用工作流程的分析等.     

基于TTCN-3的CTCS-3级列车运行控制系统自动测试方法

提出了基于TTCN-3语言的CTCS-3级列车运行控制系统的自动测试方法;该方法在考虑分布式实时系统自身复杂性和实时性等特点的前提下,首先将CTCS-3系统分解为多个实体,针对每个实体,根据功能需求规格说明书利用LPTIOA进行带时间约束信息的模型描述;然后,根据相应的算法得出测试序列及测试集;再将得到的测试序列及测试集根据规则转换成TTCN-3语言描述的测试序列和测试集;最后在基于TTCN-3测试平台中对被测实体进行测试。     

ARCNET网络系统实时性能分析与研究

列车控制网络在列车控制系统中起着非常重要的作用,其实时性能直接影响到列车的安全可靠运行。对其实时性能进行分析评价可以优化设计列车控制网络的应用层,合理配置网络,优化网络性能,从而保证列车的安全可靠运行。本文介绍ARCNET列车控制网络的数据帧类型,数据通信机制和自动重构过程等,并对ARCNET网络通信延迟时间参数进行分析,建立ARCNET网络数据通信延迟时间模型、分析其网络实时性,并提出改进网络实时性的方法。最后在搭建的网络控制系统中,对实验测试结果和模型计算结果进行比较,验证模型的正确性。并利用分析结果以及建立的通信延迟时间数学模型,计算开发基于ARCNET轻轨列车网络控制系统的轮询周期,为系统应用层设计提供依据。     

基于MVBC的分布式智能I/O模块的研究

简要介绍了新一代分布式列车控制系统的基本结构和功能，详细论述了新一代MVB通信控制器MVBC01的特点以及基于MVBC1类设备协议的分布式智能I/O模块的设计原理；最后指出该研究成果在改进现有列车控制系统的性能以及自主开发新一代列车控制系统等方面所具有的现实意义。     

严重初始延误与区间限速条件下高速列车实时调度模型

针对突发事件下列车正常秩序的快速恢复与调度优化方案的自动生成问题,现有调度优化模型与一般人工经验难以处理复杂事件场景,且求解效率较低.面向同时包括严重初始延误与区间限速影响的复杂突发事件场景,设计提出大面积列车延误和区间限速等针对性约束,构建基于事件活动网络的列车多目标非线性调度优化模型.为实现实时调度,采用添加中间决...     

基于HLA的列控系统多车仿真策略研究

基于列控系统需求进行的多车仿真研究,是构建完备的列控仿真与功能测试环境的基础环节。本文针对列控系统多节点、分布式的特点,设计基于HLA的列控系统多车仿真方案,提出两种多车仿真策略。根据不同的仿真策略构建基于HLA的多车仿真联邦的逻辑模型和高层仿真模型。对采用不同仿真策略实现的多车仿真联邦进行性能测试,实验结果表明多辆仿真车整体作为一个联邦成员加入仿真联邦的策略更适用于多车仿真,该仿真策略能够满足列控系统中多车仿真的需求。     

车车通信列控系统资源管理单元安全性分析

基于车车通信的列控系统在传统车地通信的基础上,引入了车车通信技术,后车与前车实时通信,极大地简化了地面设备,提高了列车运行效率.使用STPA法对该系统的关键设备(资源管理单元)的安全性进行研究.以资源管理单元下发临时限速命令的过程为例,识别出过程中的危险行为,找出系统的不安全因素,规划安全性设计需求.通过安全性设计需求...     

高速列车安全运行电磁控制系统的研究

提出高速列车安全运行电磁控制系统(简称电磁安全控制系统)的设计方案。电磁安全控制系统采用主动控制方式,通过对现场采集的数据信息进行解析,获得轮对间受力情况,经核心运算输出控制信息,控制执行机构动作电磁系统,使两轮对间受力趋于平衡,实现对列车运行状况的实时调整和危险情况下的自动控制。最后,从系统的实现功能入手,对其进行动态模拟,并对所得数据进行分析、对比,完成对系统性能的试验论证。     

基于Timed-UML顺序图的RBC交接形式化建模与分析

在CTCS-3级列控系统中,采用RBC技术将线路划分成多个管辖区段。当列车行驶并跨越相邻RBC交界区域时,控制权将会移交至前方相邻RBC,整个过程称为RBC交接。在运行中,RBC交接过程能否实时安全可靠地执行,直接影响着列车的行车效率和乘客的生命安全。采用一种基于添加实时约束的UML顺序图与时间自动机结合的模型来建立RBC交接场景。以双车载电台的RBC切换策略出发,建立切换的Timed-UML顺序图模型,然后按照UML-TA转换规则,建立得到完整的时间自动机网络模型。并利用UPPAAL验证工具对RBC交接模型进行形式化建模及分析,对模型的死锁和功能实现做了验证,从而达到对CTCS-3级RBC子系统的实时性以及设计规范合理性的验证目的。