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

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

一种基于场景的CTCS-3列车控制系统建模方法研究

对CTCS-3列车控制系统进行有效的测试、分析和验证是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础。本文以CTCS-3列车运行控制系统的UML非形式化模型为基础,以自动机模型作为系统形式化模型描述的数学工具,研究UML顺序图(场景)自动转化为自动机网模型的方法。首先将场景的UML顺序图自动转化为子系统的子自动机模型,然后通过合并不同场景的子自动机模型,得到子系统的组元自动机模型,最后通过对通信通道的建模得到系统的自动机网模型。使用本方法,基于系统的UML顺序图模型可以自动生成系统的自动机网模型。     

基于CPN的联锁系统选岔网络建模及验证

在详细分析联锁系统选岔电路的前提下,抽象出选岔网络的联锁逻辑条件,并采用有色Petri网(Colored Petri Net,CPN)为其建立形式化验证模型,同时采用CPN TOOLS对所建立的模型进行仿真及状态空间分析,结果表明所建立的模型能够很好的描述选岔网络的工作状态。     

联锁软件的Petri网形式化定义

用Petri网对联锁系统中的核心部分－联锁机中的联锁软件进行表式化定义和分析，以减少联锁系统中的不确定性因素，降低联锁软件的复杂性，保证联锁软件定义的正确性，并对该定义进行了形式化验证。同时以进程建立过程作为事例，说明了用Petri我形式化定义联锁软件的具体过程，采用分层模型化技术对联锁软件中的各个变迁（模块）进行逐级分解和验证，最终得到经过验证的，足够详细的联锁软件模型，利用该模型能对系统的一些重要性能（如安全性和实时性）进行分析和改进。     

全自动无人驾驶模式下系统功能与场景分析

全自动无人驾驶系统作为目前集成化、自动化程度最高的列车运行系统,能够更好地适应高密度、大客流的运营需求,代表了城市轨道交通领域的发展方向。通过全自动无人驾驶系统与传统有人驾驶系统的比较,阐述了全自动无人驾驶列车的功能和特点,并对其特有功能和场景进行分析和研究,为全自动无人驾驶系统的应用提供参考和建议。     

基于有色Petri网的RBC行车许可生成建模与仿真

CTCS-3级列控系统行车许可是保证高速列车安全运行的关键信息,及时准确地为辖区内列车计算和发送行车许可是RBC(无线闭塞中心)子系统的主要功能之一。在分析CTCS-3级列控系统不同运营场景下行车许可生成机制的基础上,采用层次化描述思想,建立基于CPN(有色Petri网)的RBC行车许可生成模型,并运用动态仿真和状态空间分析工具对模型进行了仿真分析。结果表明,所建模型能够满足不同运营场景下计算行车许可的要求,无死锁,并具有活性、回归性和公平性,为分析列控系统性能提供了很好的试验平台。     

基于Petri网列车群模型的列车运行冲突分析

列车运行冲突检测是铁路系统安全运营的重要保障。本文首先给出赋时着色Petri网的形式化定义,定义变迁使能和触发规则及状态转移函数;基于赋时着色Petri网,以库表示车站/闭塞分区,托肯表示列车,建立列车群模型,为冲突检测提供模型基础。在经典Petri网冲突定理的基础上,结合库容量约束和时间间隔约束,提出列车运行冲突判定定理,并证明该方法的正确性;在此基础上,设计基于可达树的冲突分析方法,并以太原铁路局部分线路为例,通过实例介绍列车运行冲突和进路冲突检测分析的方法。基于Petri网的列车群模型为铁路系统冲突分析问题的处理提供新的途径。     

车地协同下的联锁子系统HCPN建模与验证

联锁子系统作为站内行车安全的关键保障,是车地协同下的列车运行控制系统的重要组成部分。传统联锁子系统存在地面集中控制失效风险大、列车自主化程度低等不足,为顺应精简系统结构、降低运营成本和提升列车自主化的列控技术发展趋势,设计一种车地协同下的联锁子系统用于城际铁路。考虑多车间的进路冲突是影响子系统功能实现的关键因素,提出进路预延伸策略以避免列车间的进路冲突。为确保联锁子系统功能安全,采用一种基于层次着色Petri网(HCPN)的系统功能建模与验证方法。通过对联锁子系统的主要功能实现过程—进路建立过程进行分析,提取子系统的功能需求,以此建立顶层需求模型。为缩小底层实现与顶层需求之间的差距,建立基于数据及行为低抽象度表达的模块层模型,并在其中引入死锁控制策略实现对系统功能逻辑的完整表达。以冲突进路建立场景为模型的输入参数,执行验证过程,通过对模型标准状态空间性能分析,实现对模型正确性的检验。在此基础上,采用分支时序逻辑ASK-CTL公式与状态空间搜索算法相结合的验证方法,完成对子系统功能安全性的检验。研究结果表明:模型的行为特性同子系统预期相一致,能够正确表达系统的行为。所设计子系统满足功能安全需求,可为底层实现提供依据。     

列车运行控制系统中安全通信协议的形式化分析

安全通信协议是保证基于通信的列车运行控制系统中通信安全的主要因素,其性质和最终实现正确的形式化验证具有重要意义。本文将欧洲列车运行控制系统安全通信协议规范中的一些未强制规定的要求明确化,选择分层赋时有色Petri网(CPN)对修改后的安全通信协议进行研究,综合安全层、信道与应用层模型提出无线通信系统模型的分层结构,通过改变信道与应用层模型的参数,分析修改的安全通信协议中安全连接建立的时间特性。分析结果表明:信道丢包率为0.1、0.05、0.01的情况下,修改的安全通信协议安全连接建立时间特性是符合规范要求的。     

列车区间运行安全的Petri网模型研究

鉴于我国铁路列车行车事故多发生在区间运行过程中,以及列车在区间运行的动态特性,利用Petri网具有强大的功能描述及分析系统动态变化的特点,建立了列车区间运行系统的动态Petri网模型。通过对该模型合理性的论证,并运用此模型对实际事故案例进行分析,表明所建的列车区间运行安全Petri网模型是合理的。     

基于UPPAAL的FAO系统典型运营场景建模与验证

全自动驾驶系统FAO(Fully Automatic Operation)具有安全、可靠、高效的特点,成为未来城市轨道智能交通系统的主要发展方向。FAO系统典型运营场景是1个实时的过程,为发现其逻辑的错误、功能和性能的缺陷,需要在系统设计前,针对系统需求规范中典型运营场景的实现流程进行形式化分析。本文分析FAO典型运营场景保护区的实现流程,在系统需求规范中提取其功能与性能的需求,采用基于时间自动机理论的UPPAAL构建时间自动机网络模型,进行仿真分析,并验证其功能属性、性能属性与安全属性。通过反例分析、模型修正,增强对FAO系统的理解,减少设计故障,提高安全性,为系统设计与实现打下良好的基础。     

轨道交通无人驾驶顶层设计要素分析

文章通过对无人驾驶轨道交通车辆的应用场景进行系统性分析,结合国内和国际相关列车使用情况,在安全、场景交互、系统协同、系统冗余、智能监控5个维度提出无人驾驶轨道交通的顶层设计要素,为指导国内轨道交通无人驾驶的规划、运营提供参考。     

面向全自动运行的城轨交通火灾联动方案设计与建模验证

全自动运行是未来城市轨道交通发展的主要方向，与传统驾驶模式相比，对于特殊运行场景下的应急处理能力与处理效率有着更高的要求。本文基于列车发生火灾的特殊运行场景，区别于以往由调度人员作为综合监控系统与列车自动监督系统的联动桥梁，设计了全自动驾驶场景下的火灾联动方案，确定了火灾报警系统的火灾识别流程、列车控制管理系统的数据转发和应急控制流程、运行控制中心的火灾响应流程，以及各系统之间的通信校验流程；同时，使用基于时间自动机理论的UPPAAL工具，对从火灾识别到火灾应急响应的全过程进行了形式化建模分析，并且对该联动方案的安全性和功能进行了形式化验证。验证结果表明，该联动方案能够有效地满足各个系统之间的联动要求，为全自动驾驶模式下的非正常运行场景的应急联动处理打下基础。     

城市轨道交通全自动运行系统及安全需求

结合国内外全自动运行系统的运营研究资料,介绍国际轨道交通全自动运行系统发展状况,探讨全自动运行系统的功能结构。结合IEC62267与IEC62290等国际标准,论述全自动运行系统典型的系统功能与安全需求。以系统FAM与CAM模式转换为例,对运营场景进行分析研究,如实反映列车全自动驾驶系统真实的运营过程,在建模之前需对系统的功能进行梳理,实现需求到场景的追踪,以确保所建模型与功能需求的一致性,即此模型表达系统最终需要完成哪些功能,这些功能之间的关系如何以及系统完成这些功能需要与哪些外部参与者或系统实现交互。对全自动运行系统展开深入而全面的研究,对我国自主研发全自动运行系统提出参考建议,为全自动运行系统的安全运营保驾护航。     

面向RITS的多Agent列车群运行模型

基于RITS的分布式系统结构和智能属性特征,针对列车群运行系统中子系统之间的关系描述以及通信协作行为的建模问题,采用面向Agent的G-Net方法构建了一种多Agent的列车群运行模型(AGNTOM)。该模型体现了多Agent技术、G-Net(Petri网)形式化描述、便于分析等特点,不仅能够描述列车Agent与车站Agent在列车运行过程中的通信能力,而且能使用形式化方法确保模型的各种属性。对模型所描述的列车与车站之间的通信协商过程采用基本Petri网模型描述,并使用已有的Petri网分析方法进行相关属性的分析。研究结果表明:模型具有L3-活性;模型所描述的列车和车站之间的通信协商行为不会导致通信的死锁与阻塞等。     

基于停站方式最少的高铁停站方案优化研究

合理确定列车停站方案对提高高铁运输组织水平具有重要的现实意义,既有研究中构建的模型容易导致列车停站方案中停站方式数量较多,不利于运行图编制及能力利用。针对该问题,以列车停站方式最少为目标,对高铁列车停站组合进行优化研究,构建了高铁停站方案优化模型。以京沪高铁为例进行案例研究,通过与既有停站方案进行对比分析,发现采用优化方案停站方式减少了5种、列车因停站总延误时间减少了119min、车站服务频次和直达列车分布满足旅客需求,验证了模型的有效性与实用性。     

基于Petri网列车连挂解编模型分析

提出一种基于Petri网描述系统的方法,该方法(简称EPN)将Petri网与UML思想相结合,通过5种简单的事件模型来分析系统.由于借鉴了UML思想,使得EPN易于对一些复杂系统进行描述,也易于利用UML分析结果对系统快速建模.同时EPN是基于Petri网,因此完全可以利用现有Petri网的数学模型和工具进行建模和仿真.本文主要对列车控制系统中的连挂和解编过程进行建模.通过模型验证采用EPN分析系统的有效性和便捷性.     

城市轨道交通全自动无人驾驶系统与传统CBTC系统差异分析与探讨

随着城市轨道交通的快速发展,全自动无人驾驶系统已成为大力发展的方向,是城市轨道交通未来发展的重点。对全自动无人驾驶系统与传统基于通信的列车控制系统(CBTC)在系统组成、主要功能点及应用场景等方面的差异进行分析,总结全自动无人驾驶技术的优势和主要功能特点,提出针对全自动无人驾驶系统主要功能点的设计思路,为实现高度自动化、高度集中控制的全自动无人驾驶系统提出功能和接口设计的相关建议。     

基于SPN的CTCS无线通信形式化建模与分析

CTCS-4列车运行控制系统是基于无线通信传输信息的系统,其无线通信系统是一个动态、复杂的分布式系统,正确的形式化验证对于其性质和最终实现具有重要意义。本文主要考虑高速列车在移动闭塞区间条件下CTCS无线通信的形式化建模和可靠性分析,建立随机Petri网(SPN)表示的CTCS无线通信机制模型和列车与无线闭塞中心通信的GSM-R故障恢复模型,给出对通信故障定位的表示方法,并采用TimeNET仿真工具对GSM-R通信系统的可靠性进行分析得出相应结论。分析结果表明,列车在500 km/h的速度下,越区切换成功概率为99.45%,连接丢失概率为10-2/h。最后,本文将分析结果与GSM-R的技术标准进行比较,说明其可靠性满足规范要求。     

基于Petri网模型的高铁6‰下坡道延续进路防护方法

针对大于6‰下坡道高铁车站的延续进路防护问题，以成兰线某车站为例，研究基于Petri网模型的防护方法。以车站平面布置图为依据，建立相应的延续进路防护资源分配约束模型，包含6‰下坡道防护模型和延续进路防护故障诊断模型。通过6‰下坡道防护模型对延续进路涉及到的轨道区段占用权进行分配，实现延续进路的安全性防护；延续进路防护故障诊断模型采用形式化验证方法，通过被标记的故障库所对不可行的延续进路排列报错，实现延续进路运行计划的安全性验证。利用Petri网的可达性、有界性、安全性，对车站延续进路可能产生的列车碰撞和冲突进行仿真验证，验证结果可为列车运行计划的排列提供参考。