系统理论过程分析在城市轨道交通列车运行控制系统设计中的应用

使用STPA(系统理论过程分析)安全分析方法,针对北京燕房线实际设计案例中的典型系统级危险源,选取列车进站停车运营场景建立相应的分层控制结构模型,辨识不安全控制行为,分析列车运行过程中的危险致因和安全约束,结合实际工程项目转化为切实可行的安全需求和防护措施。表明STPA方法分析过程全面深入,不仅可以分析技术系统,还可以分析运营组织中的人为因素,可以更加全面辨识运营场景中所涉及的危险致因。     

基于Petri网的全自动无人驾驶列车停站场景形式化建模与验证

为进一步提高全自动无人驾驶系统的安全性,采用Petri网理论在全生命周期早期对系统运营场景的实现流程进行形式化建模与验证。选取正线运营中的列车停站这一典型运营场景,进行对象提取与状态分析,结合各对象与库所、变迁的对应关系,建立Petri网模型,并利用仿真软件PIPE对其有效性和正确性进行形式化验证。针对可能出现的异常情况对模型进行优化,设置车门与站台门开关时序,避免乘客拥挤时出现安全隐患。试验结果表明：建立的Petri网模型有界、安全且无死锁,满足列车停站场景功能需求,模型的可靠性和有效性得以验证,为全自动无人驾驶系统的开发应用与安全分析提供理论支撑。     

需求阶段的无线闭塞中心交接危险因素分析

根据STAMP理论分析需求阶段的RBC交接危险因素,利用分层控制框图对RBC交接过程的控制关系进行描述;使用混成自动机对其中的控制算法、组件状态变化进行建模;给出控制结构中过程模型的形式化定义,并使用对象约束语言OCL对过程模型进行构建。根据需求阶段的控制缺陷分类,利用人工分析和形式化分析相结合的方式,分别对与输入相关、与功能模块相关以及与系统需求规范相关的危险因素进行分析。通过结果对比发现,本文所提基于STAMP理论的方法适用于需求阶段的RBC交接危险因素分析。     

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

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

面向高速铁路信号系统安全分析的UML扩展设计研究

设计面向高速铁路信号系统安全分析的专用建模语言和建模方法,对于提升安全分析结果准确性具有重要意义。根据高铁信号系统STAMP安全分析模型的构成,提取该安全分析模型的特征元素。基于模型特征元素,利用UML扩展机制实现UML类和关系的构造型设计,并采用对象约束语言作为模型约束条件,设计面向高铁信号系统STAMP建模的UML建模语言。最后应用于高铁信号系统典型场景安全分析模型的构建。     

高速铁路列控系统运营场景实时性的建模与验证

高速铁路列控系统是一个典型的分布式实时系统,其时间约束主要反映在运营场景中子系统之间的交互过程中。时序逻辑的扩展方法并不能完全满足描述分布式实时系统性质的需要,并且随着系统的复杂性提高,列控系统运营场景中诸如超时、期限、直到…才等形式化描述与验证上存在不足。本文提出一种适合于列控系统场景建模与验证的方法,其核心思想是使用混合通信顺序进程HCSP(Hybrid Communicating Sequential Process)形式化描述分布式实时系统模型,提出转换规则,转换成时间自动机网络模型并进行自动验证。最后通过对典型场景无线闭塞中心RBC(Radio Block Center)切换的相关属性进行建模与验证,分析证明方法的有效性。     

基于STAMP-DEMATEL的既有建筑改造安全事故致因研究

城市更新背景下既有建筑改造将是大势所趋,而既有建筑改造安全事故逐年增多,危害到国家、企业和个人生命财产安全。厘清既有建筑改造安全事故的致因并针对性防范,对降低安全事故的发生频率具有重要现实意义。基于STAMP模型,分析并构建既有建筑改造项目安全事故的分层控制结构,并以此为框架识别和筛选事故致因因素;运用DEMATEL算法分析安全事故系统各层级致因因素之间的关联关系,辨识关键性致因因素;以泉州XJ酒店改造工程坍塌事故开展案例研究,验证STAMP-DEMATEL模型的适用性。结果表明：既有建筑改造项目分层控制结构包括物理层、现场基础层、运营层、政府及社会层等4个递进层级;政府社会层如五方责任主体监督监管失察、既有建筑改造施工标准体系不健全、企业行为规范缺失等原因因素属于导致既有建筑改造事故发生的高效力因素;物理层、基层如钢柱板件严重变形、应急预案缺失、改造技术方案安全性缺失、施工机械选择不当等结果因素属于诱发事故的直接因素;基于STAMP和DEMATEL的分析结果与案例事故报告高度贴合。所构建的安全事故致因模型可用于指导既有建筑改造施工安全管理。     

基于STPA与多智能体的列控运营场景危险分析及仿真验证方法

针对列控系统运营场景危险行为与危险致因辨识的复杂性特征及其缺乏有效的仿真验证手段等问题,考虑致因因素间呈现的非线性特点,提出1种将系统理论过程分析(STPA)方法与多智能体仿真技术相结合的列控运营场景危险分析及仿真验证方法.以单电台无线闭塞中心(RBC)切换场景为例,构建分层控制多智能体结构模型,利用STPA方法辨识R...     

基于多层STAMP模型的CTCS-1级列控系统功能安全分析方法

根据CTCS-1级列控系统总体设计方案,以安全控制为核心,结合系统理论事故模型和控制过程提出多层STAMP模型与相应的安全分析方法。利用UML语言对列控系统内部组件交互控制过程进行描述并将其转换为多层STAMP模型和故障分析模型,分析危险事件产生原因,实现对系统功能的安全分析。以CTCS-1级列车进站场景为例,建立多层STAMP模型并针对可能发生的危险事件进行系统功能安全分析。分析结果表明,多层STAMP模型和安全分析方法适用于CTCS-1级列控系统的功能安全分析。     

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

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

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

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

全自动运行系统场景验证平台及其应用

全自动运行系统运营场景定义对于全自动运行项目建设和运营非常重要.介绍了一套可以用于验证全自动运营场景的平台;描述了全自动运行系统场景验证平台需求、建模方法、平台结构及核心技术;举例说明了该平台如何应用于全自动运行系统的场景验证.     

无人驾驶地铁人员防护开关方案研究

为实现无人驾驶地铁全自动运行区运营人员的安全防护,对无人驾驶地铁人员防护开关使用场景、功能要求、设置原则、实现方式等进行研究,给出无人驾驶地铁人员防护开关实现方案。     

城轨交通全自动运行系统组合测试用例生成方法

为提高城轨全自动运行系统测试的全面性，结合时间自动机建模方法和组合测试理论，提出全自动运行系统组合测试用例生成方法。首先，以全自动运行系统运营场景为测试建模对象，基于时间自动机建模方法，描述全自动运行系统的运营场景，利用Yggdrasil生成100%满足运营场景时间自动机模型节点覆盖和边覆盖的测试路径；其次，采用输入域建模理论，提取测试路径反映的系统工况作为组合测试的输入参数，利用组合测试算法生成全自动运行系统的组合测试用例；最后，以全自动运行系统中的唤醒场景为例，采用UPPAAL从ATP、ATO、TCMS、AOM和车辆5个方面建立唤醒场景的时间自动机模型，以向前跳跃失败为例，采用2-维组合覆盖生成组合测试用例。结果表明，测试用例100%覆盖测试模型所有的边和节点，以及测试模型任意2个输入之间的组合，提升了全自动运行系统测试的完备性。     

CTCS-3级列控系统规范建模与验证

结合统一建模语言UML与符号模型检验SMV形式化方法,提出需求规范严格建模和验证方法。利用需求管理工具,保证了模型和规范的一致性和对规范的覆盖性,同时实现了规范验证结果对模型、转换规则和规范的跟踪。给出了CTCS-3级列控系统严格建模与验证的方法体系和流程,并以CTCS-3级列控系统需求规范中的模式转换部分为例,说明了规范的建模、验证和分析过程。     

基于Prover的联锁软件形式化验证过程研究

计算机联锁系统是铁路信号控制系统的核心设备,是有着苛刻安全要求的复杂控制系统。本文采用Prover形式化开发工具对联锁软件安全需求进行形式化验证。通过模型检验的形式化验证方法,遍历系统输入变量的所有状态空间.验证联锁特定应用满足系统安全需求,确保系统的安全性得以正确实现。在保证系统安全性的基础上,以全状态空间查找反例的检验方法进一步提升产品的质量。     

基于SSM-HAZOP的自主化ATP等级转换功能建模与验证

针对高速铁路列控系统安全完整性等级要求高、安全功能需求验证难等问题,考虑列控系统安全需求建模具有层次性、并发性等特点,以自主化ATP等级转换功能为例,综合运用安全状态机(SSM)建模理论,以及危险与可操作性分析方法 (HAZOP),提出一种基于SSMHAZOP的建模与自动验证方法。首先建立等级转换功能的SSM模型,然后基于HAZOP方法提取安全属性,最后利用SCADE DV工具自动验证等级转换的安全需求。结果表明,该方法能够满足列控系统等级转换安全需求建模与验证的要求,可应用于自主化ATP的安全验证。     

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

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

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

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

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

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