基于Timed RAISE的高速列车RBC切换协议形式化建模及验证

在CTCS-3(Chinese Train Control System Level 3)级列控系统中,RBC(Radio Block Center)切换是影响列车安全高效运行的重要环节,现阶段对RBC切换协议进行验证分析所使用的形式化方法还存在状态爆炸或描述性质单一等问题。基于Timed RAISE的形式化方法,结合域的模型,在对RBC切换流程分析的基础上,构建状态转移图,得到切换协议的形式化模型,使用等价和推断的推理规则对模型的正确性和实时性进行推理验证,得到的结果表明,RBC切换协议满足规范标准对正确性与实时性的要求,将验证结果与其他文献的结论进行比较分析,说明该方法具有通用性,对于推广其在列控系统场景验证中的应用有一定的实际意义。     

Timed RAISE方法在列控系统等级转换场景中的应用研究

高速铁路列车运行控制系统是一个复杂的实时性系统,结合其实际特点,将域方法作为系统描述的切入。通过对模型检验和定理证明两种验证方法的分析比较,提出使用基于定理证明的时间化工业软件工程的严格方法Timed RAISE形式化方法对等级转换(CTCS-2级至CTCS-3级)场景进行描述,并对其场景交互一致性和实时性进行验证,结果表明该场景不会出现场景交互一致性错误,也不会违反时间的约束。     

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

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

基于时间自动机的自主化ATP等级转换功能建模与验证

自主化ATP(列车自动保护)系统在国产化ATP系统的基础上,增加了一些新的功能需求。针对自主化ATP系统安全关键功能的安全性和正确性保障的问题,以自主化ATP系统中典型的C2等级转换C3等级的等级转换功能为研究对象,采用时间自动机形式化地分析等级转换功能的安全性、活性和实时性。研究时间自动机的数学理论基础,分析自主化ATP系统等级转换功能的逻辑和与其他系统的数据交互;采用时间自动机建模方法,从ATP、RBC(无线闭塞中心)和应答器3个方面,建立C2等级转换C3等级的时间自动机模型;研究自主化ATP系统等级转换功能需要满足的安全性、活性和实时性要求,利用UPPAAL软件验证等级转换功能的系统性质。结果表明,自主化ATP系统C2等级转换C3等级功能满足期望的系统需求。     

等级转换的特殊应用场景分析

高速铁路动车组能够根据线路的列控系统等级自动切换车载设备的列控系统等级。在工作中发现等级转换的设计在一些特殊场景中受到某些因素影响,而这些因素在既有原则规范中并未提及或详细说明。通过分析在特殊场景中这些因素的影响范围、与原则规范的关系及克服影响的办法,总结得出可实际应用的新设计建议,并指出等级转换的设计原则在工程项目中需进一步研究完善。     

属性驱动的列车控制系统需求建模与验证

形式化语言越来越多地用来描述列车控制系统需求规范,其精确的语法和语义一方面有助于创建精确的需求模型、消除理解差异,另一方面也为进一步分析验证提供了基础.通过提出一种基于属性的需求分析方法,利用具体的形式化技术来分析需求.首先将由自然语言描述的需求规范转换为属性描述语言(PSL)形式化规范,并通过仿真和博弈分别进行语义检查和可实现性验证,最后通过断言来检验形式化语言所刻画的系统的精确性和完整性.该方法从自然语言形式的需求约束中直接提取相关需求规范,构造形式化模型并进行验证,为需求的早期确认提供了一种新的实用途径.并以CTCS-3级列控系统RBC切换场景为例,说明该方法的有效性.     

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

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

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

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

基于UML的列车运行监控装置功能建模分析

既有线铁路系统运营场景复杂，运营需求多变，导致列车运行监控装置（LKJ）功能需求变化频繁，为了合理、规范地管理功能需求，有必要基于UML对LKJ功能进行建模研究。通过分析LKJ的结构与功能，建立了系统的用例模型；利用UML语言中的类图、顺序图和状态图，分析LKJ主要运营场景的静态结构与动态行为，并由此建立各场景的静态模型和动态模型；最终对所建LKJ功能模型进行验证，确保模型的正确性和完整性。利用所建的LKJ功能UML模型，能避免对LKJ功能需求的歧义理解，有利于开发与维护工作的顺利进行。     

基于TA的等级转换场景变异测试方法研究

针对等级转换场景下的变异测试集不完备问题,提出基于时间自动机(Time Automa-ta,TA)的等级转换场景变异测试研究方法.该方法结合时间自动机理论和等级转换操作流程建立TA模型,同时设计15种变异算子对模型进行变异测试,通过计算加权变异分数评估测试案例集的完备性,并对加权变异分数较低的算子进一步修改补充,最终得...     

基于UML与CPN的CTCS-3级列控系统建模与验证方法研究

CTCS-3级列控系统安全功能极其复杂,为保障其正常运转,有必要对列车运行控制系统的建模与验证进行深入研究。在分析了UML建模图和有色Petri网优缺点的基础上,提出了UML和有色Petri网(CPN)相结合的建模与验证方法,并应用在CTCS-3系统中,对CTCS-3级列控系统的建模与验证具有积极的研究意义。     

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

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

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

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

列车通信网络控制器的综合验证

列车通信网络对安全性和可靠性提出更高的要求,如何保证网络控制器设计的正确性和可靠性成为确保列车安全运行的关键因素之一。本文以高级验证方法学为指导搭建列车网络控制器的层次化验证环境,提出网络拓扑级验证模型和错误注入机制,并对验证结果进行深入分析。实验结果表明:该验证方法增强验证组件的重用性,弥补传统方法的不足,有效提高了验证效率。     

基于场景法的列控系统等级转换功能测试用例设计

为了改善当前列控系统等级转换功能测试用例覆盖不全面的问题,以CTCS-2级转CTCS-3级功能为研究对象,采用场景法分析转换逻辑,设计测试用例。首先,分析CTCS-2级转CTCS-3级的功能逻辑;然后,介绍场景法设计测试用例的过程及基本流和备选流划分原则;最后,采用场景法对CTCS-2级转CTCS-3级过程中的基本流和备选流进行划分,确定基本流和备选流有向图,设计测试用例。结果表明,该方法设计的测试用例能够提高列控系统功能性和安全性测试的完备性,从而保障列控系统产品的质量。     

基于图论和面向对象的列控数字轨道地图研究

将全球定位系统(GPS)和地理信息系统(GIS)结合在一起应用于轨道交通中,可提高列车定位精度、减少轨旁设备、降低建设和维护成本。一份结构合理的数字轨道地图可以提高列车定位的实时性和准确性。本文主要研究数字轨道地图的模型、设计和验证。首先,结合拓扑关系数据模型和面向对象数据模型的优点,对数字轨道地图进行建模;基于图论和面向对象的数据结构的思想,利用空间数据和对象属性数据实现数字轨道地图的设计。其次,结合图的深度优先搜索算法,提出对数字轨道地图连通性、合理性和正确性进行验证的算法。最后,本文在VC++平台下实现数字轨道地图的功能,并采用丰沙线三家店车站现场采集的GPS数据对数字轨道地图进行实验验证。结果表明本文提出的设计方法是可行的。     

CTCS-3至CTCS-2等级转换应答器组布置

CTCS-3至CTCS-2级列控系统等级转换应答器布置非常重要。等级转换应答器布置不当,会引起列车紧急制动。通过对CTCS-3级列控系统应答器应用原则研究,介绍CTCS-3至CTCS-2等级转换应答器组布置原则,并详细分析特殊场景下引起列车紧急制动的原因。最后结合特殊场景,提出优化等级转换应答器布置的方法。