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

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

基于UPPAAL的LKJ-15系统模式转换功能建模与验证研究

模式转换是LKJ-15系统的重要功能。为了保证模式转换功能安全,提出利用形式化建模工具UPPAAL对该功能进行建模与验证。首先分析LKJ-15系统各种模式转换条件,建立模式转换信息交互网络;之后使用UPPAAL建立模式转换功能模型;最后对模型进行仿真和BNF语句验证。结果表明:该模型满足LKJ-15模式转换的功能要求,其安全性得以验证,为系统开发和应用提供了理论保障。     

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

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

根竹站ATP等级转换紧急制动的分析处理

本文针对广西玉林开通动车组列车后,在黎湛线根竹站发生紧急制动的故障实例,通过下载动车组ATP运行记录数据,结合地面应答器报文数据进行综合分析,判断故障为200C型ATP在处理地面应答器报文描述的线路数据信息的逻辑上存在缺陷。提出了修改地面应答器报文或修改ATP设备软件逻辑两种解决方案,并进行修改地面应答器报文试验,彻底解决了该问题,确保了动车组列车的安全。     

基于时间自动机的CBI道岔转换时间建模与验证

针对CBTC计算机联锁安全性十分重要的问题,介绍时间自动机理论,分析CBTC计算机联锁系统的结构和与传统联锁系统的区别,以CBTC联锁系统的道岔转换功能为例,采用UPPAAL建立了道岔转换模型,分析模型的安全需求。表明了在联锁系统开发过程中采用基于时间自动机建模与验证的方法的可行性和有效性。     

ETCS等级转换功能研究

为了满足列车在不同等级线路上运营的互联互通需求,对于具有多种等级控车功能的列车,应实现其在不停车情况下的自动等级转换功能,因此对等级转换功能进行深入的研究具有重要的意义。采用数学模型分析的方法,借助欧洲列车运行控制系统ETCS作为研究平台,对等级转换功能及相关要求进行了一些系统性的分析和研究,该分析结果同样适用于其他列控系统的等级转换功能。     

基于UML语言的CTCS-1级车载ATP功能建模分析

分析CTCS-1级车载ATP的硬件结构和功能需求,建立系统的用例模型;从系统运营场景出发,划分系统功能的参与者,定义参与者的属性和行为,由此建立了场景类图模型和系统类图模型;利用活动图和时序图,从不同角度描述了系统功能参与者间的交互情况;借助编程语言对所建功能模型进行了验证。     

自主化制动控制电磁阀设计与试验验证

文章介绍了针对标准地铁列车研制的自主化制动控制电磁阀,阐述了其结构组成和工作原理、主要参数要求、关键部件设计及计算仿真,并通过试验研究验证了自主化产品的性能与参数。试验结果表明自主化产品与进口产品性能相当,可以满足标准地铁列车制动系统的使用需求。     

ATP接口仿真及功能验证系统应用研究

ATP设备是保障高速列车行车安全的关键设备,围绕ATP设备的测试验证、检修分析、隐患排查等日常维护管理是电务段的重要工作。本文结合站段的实际维护经验及产品应用情况,详细阐述了CTCS-3级ATP接口及功能验证系统的需求来源、系统方案及应用场景等,该系统在ATP设备的日常维护和职工教学培训中发挥了重要作用。     

基于TRSL的RBC等级转换场景研究

无线闭塞中心等级转换场景作为中国列车运行控制系统主要场景之一,切换成功与否直接影响高速列车的安全和运行效率。通过对形式化验证方法的分析,采用基于定理证明的时间化工业软件工程规范语言的严格方法(Timed Rigorous Approach to Industrial Software Engineering Specification Language,TRSL),在对等级转换过程进行分析的基础上,设计交互信息图,构建状态迁移图,并结合域建模方法实现对该场景的TRSL描述,最后利用语言推理规则,结合系统特性,实现对切换正确性和实时性的双重验证,结果表明:该场景满足系统规范对功能性和实时性的要求,继而说明该方法的有效性、正确性和通用性,为我国列控系统的设计开发和验证提供一种新的途径和依据。     

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

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

基于UPPAAL的列车自动防护系统形式化建模与验证

本文分析列车自动防护(ATP)系统的结构和功能需求,建立系统的时间自动机模型,采用UPPAAL模型验证工具对模型的活性和安全性进行验证.结果表明,采用时间自动机对安全苛求实时系统进行建模与验证,可以有效地保证系统的可靠性和实时性.     

基于UPPAAL的列控系统临时限速建模与验证

临时限速系统是列控系统的重要组成部分,是符合故障-安全准则的安全苛求系统。文章基于临时限速技术规范和时间自动机理论,分析临时限速系统的组成结构,提取其功能和性能约束,利用UPPAAL工具对其信息交互行为进行建模仿真,验证该系统的实时性,为进一步完善临时限速系统的设计与开发提供参考。     

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

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

基于RFM模型的商场会员画像的建模与验证

针对某大型百货商场会员画像描绘中的聚类问题进行研究,阐述RFM模型构建用户聚类的建模方法和实现的过程。采用最近消费时间、某段时间间隔内消费次数、消费总金额为模型的三个指标,利用Python软件的K-means算法完成聚类实验。实验结果证明K-means算法很好地实现了聚类性能,同时表明所提出的RFM模型建模方法对会员画像描绘是有效的,从而为商场制定有针对性的会员营销策略提供数据支撑。     

基于MSC与UPPAAL的高铁跨界临时限速建模与验证

临时限速服务器是高铁列控系统的重要组成部分,其不仅要校验CTC下发的临时限速命令,还要与相邻调度台临时限速服务器之间进行频繁的信息交互,因此对其安全性和实时性要求也更苛刻。为了满足高铁列控系统对其运行的要求,采用时间自动机理论和消息顺序图(MSC)相结合的方法,首先建立跨界临时限速命令的MSC模型和时间自动机子模型,再利用UPPAAL验证工具对形式化语法BNF描述的时间自动机子模型属性进行验证。根据仿真验证结果确认了跨界临时限速信息的安全性和受限活性,为进一步开发临时限速服务器功能提供了重要的依据。     

时速250km等级动车组自主化车轮的耐磨性能试验研究

对时速250km等级动车组自主化D1车轮进行耐磨性能试验,并与进口ER8车轮的耐磨性能进行对比。首先在实验室内采用Amsler磨损试验机对这2种车轮试样进行磨损试验,测量各试样的磨损失重量。然后将这2种车轮安装在同一动车组上,在太原南至永济北区间往返运行,通过计算车轮踏面廓形实测线与基准线滚动圆中心位置纵坐标的差值,衡量车轮实际的磨损量。结果表明:自主化D1车轮试样的相对耐磨性能约为ER8车轮试样的1.09倍,且其磨损机理主要为疲劳磨损,同时伴有磨粒磨损的特征;随着运行里程的增加,车轮每万km的平均磨损量逐渐减小,当运行里程达到20万km时,自主化D1车轮每万km的平均磨损量为0.041mm,低于ER8车轮,表明自主化车轮的耐磨性能较进口车轮更为优异。     

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

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

移动授权的形式化建模与验证

基于通信的列车运行控制系统(Communications-Based Train Control System,CBTC)相较于传统的基于轨道的列车运行控制系统,无论是从功能方面还是性能方面都有了很大的改进。在系统的研发过程中,对其进行建模和验证,能够发现系统设计的缺陷,进而保证系统的安全性和功能性。移动授权(Movement Authority,MA)是CBTC系统的核心功能,用来保证列车的安全运行间隔。通过对移动授权生成原理的研究,采用时间自动机和其自动验证工具UPPAAL对其进行建模以及验证,验证结果表明,搭建的移动授权模型能够达到规定的安全要求和功能要求。因此UPPAAL能够对复杂的实时系统进行仿真验证。