ctcs―3级列控系统临时限速建模和验证

《ctcs―3级列控系统临时限速建模和验证》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、CTCS―3级列控系统临时限速建模和验证摘要：为了满足临时限速系统的实时性要求，采用时间自动机理论，对CTCS3级列控系统临时限速工作流程分别建立了各设备的时间自动机子模型，进而构成临时限速系统的时间自动机网络模型，并基于临时限速系统技术规范的参数对模型进行赋值；采用BNF语法对临时限速系统待验证的属性进行了形式化描述，并应用UPPAAL验证工具对临时限速模型的安全性和受限活性进行仿真验证.验证结果表明：与现有临时限速系统的时间参数设置相比，修正后的时间参数设置避免了出现系统死锁现象；在不影响安全功能属性和受限

2、活性的基础上，提高了临时限速系统的实时性，可在规范规定时间5s内做出响应.关键词：CTCS3级列控系统；临时限速；时间自动机；UPPAAL；实时性中图分类号：U283.4文献标志码：AModelingandVerificationofTemporarySpeedRestrictionofCTCS3TrainControlSystemYUANLei1，WANGJunfeng1，KANGRenwei1，LJidong2（1.StateKeyLaboratoryofRailTrafficControlandSafet

3、y，BeijingJiaotongUniversity，Beijing100044，China；2.NationalEngineeringResearch17CenterofRailTransportationOperationandControlSystem，BeijingJiaotongUniversity，Beijing100044，China）Abstract：Inordertomeettherealtimeperformancerequirementofatemporaryspeedrestricti

4、on（TSR）systemofChinesetraincontrolsystemlevel3（CTCS3），timedautomatasubmodelsofeachequipmentofthetraincontrolsystemwereestablishedfortheworkingprocessofTSR，andatimedautomatanetworkmodelwasbuiltthroughparallelcompositionofthesubmodelstovaluatethesubmodelsusing

5、theparametricconfigurationofthespecificationofCTCS3.Then，thepropertiesoftheTSRsystemsuchassafetyandboundedlivenesswereexpressedinBackusNaurform（BNF）andvalidatedthroughformalverificationsimulationusingtheUPPAALintegratedtool.Theresultsshowthatcomparedwiththep

6、arametersdefinedinthesystemspecifications，themodifiedtimeparameterscanfixthedeadlockproblemofthesystem，andimprovetherealtimeperformanceoftheTSRsystemonthepremiseofkeepingthesystempropertiessuchas17safetyandboundedliveness.TheTSRsystemcanrespondtoinputswithin

7、5sandmeetthesystemspecifications.Keywords：CTCS3traincontrolsystem；TSR；timedautomata；UPPAAL；realtimeperformance临时限速是指线路规定限速以外具有时效性的限速，包括施工、维修引起的计划性限速，以及自然灾害、设备故障引起的突发性限速等[1].临时限速是突发的和偶然的，仅在一定的时间范围内有效[2].因此，临时限速系统是典型的实时系统，临时限速命令的拟定、设置、传输、接收、执行、确认、取消等，具有严格的逻辑顺序

8、关系和精确的时间约束特性.临时限速工作流程依据技术规范而实现，如果技术规范存在缺陷，则会危及行车安全或影响行车效率.对临时限速工作流程的实时性进行分析研究，以验证技术规范的正确性具有重要意义.目前，对临时限速的研究主要集中在介绍临时限速的应用现状[1]、分析临时限速对列车运行的影响[2]等方面.17临时限速系统具有严格的连续时间约束特性.要实现临时限速功能，涉及多个设备，表现出复杂的交