高卓凡,何 涛,姜 飞,吴永成
(1. 兰州交通大学 自动化与电气工程学院,兰州 730070;2. 甘肃省工业交通自动化工程技术研究中心,兰州 730070;3. 甘肃省轨道交通信号与控制评测行业技术中心,兰州 730070)
随着我国铁路网不断向着高效快捷、分布辽阔的方向发展,目前我国在既有线改造及客运专线建设中已使用CTCS-3级(Chinese train control system level three)列控系统。青藏铁路格拉段于2006年7月开通,其信号系统采用美国通用电气公司的增强型列控系统(incremental train control system,ITCS),并且通用电气公司对其安全保障承诺至2024年。针对青藏铁路存在地理环境恶劣、行车密度低、轨旁维修困难、与标准体系不兼容等缺陷[1],2020年中国国家铁路集团有限公司组织制定了新型列控系统(Chinese train control system-new,CTCS-N)的技术条件[2]。
CTCS-N系统符合既有CTCS的总体架构,具有无线通信、移动闭塞、列车多源融合定位、取消轨道电路等特点[3]。系统由车载设备和地面设备两部分组成:车载设备由列尾设备、列车自动防护系统(automatic train protection,ATP)、车载主机构成;地面设备由轨旁设备、列控联锁一体化系统(train control center and interlocking integrated system,TIS)、无线闭塞中心(radio block center,RBC)、临时限速服务器(temporary speed restriction server,TSRS)构成。CTCS-N具有少轨旁、高效率的特点,以车载设备为中心,将列控系统的功能进一步集中到车载设备中[4]。等级转换场景是车地交互的典型场景,有严格的时间约束,对它进行形式化建模不仅可以证明等级转换的正确性,更可以确定整个车载设备的可靠性[5-6]。
目前针对CTCS-N建模与验证的研究较少,但是针对CTCS-3的建模与验证研究已经趋于成熟。大量的研究方法表明,形式化的建模方法更适用于列控系统。形式化建模的方法有着色Petri网(hierarchical coloured petri net,HCPN)[7]、时间Petri网(timed petri net,TPN)、时间自动机(timed automata,TA)等。孙维正等[8]基于统一建模语言(unified modeling language,UML)与层次赋时有色Petri网(hierarchical timed colored petri nets,HTCPN)相结合的方法构建区域控制器(zone controller,ZC)切换场景的模型,并在CPN Tools仿真平台上进行了验证;张振海等[9]基于TA对具体场景下CTCS-3系统功能是否符合其系统规范进行建模与验证,并进行了仿真验证。其中TA可以刻画系统的连续时间特性和信息交互特性,并且有专门的验证工具UPPAAL,所以十分适合列控系统的建模。本文基于时间自动机理论对CTCS-N的等级转换流程进行建模,并利用UPPAAL进行仿真分析,最后按照正常模式和故障模式下车载设备转换的功能与性能需求验证该模型。
时间自动机通过在传统自动机的状态和变迁中添加时间约束,实现对实时系统进行建模和验证。时间自动机包含若干个时钟,系统开始启动后,这些时钟以相同的速率运行,并且在任意位置的变迁时钟都可以进行重置[10]。
时间自动机通常用一个六元组
对于复杂系统,分别对该系统的子系统进行建模,再将模型组合起来,此时各个子系统的模型存在同步通信的行为,可以用积的形式来描述整个系统[11]。
UPPAAL是一个专门用于实时系统建模和验证的工具,可以使用建模语言来描述时间自动机的积,各个子系统之间的信息通过全局变量或者同步通道来实现[12]。UPPAAL主要包含三部分:编辑器使用TA语言描述需要建模分析的系统,模拟器利用模型仿真来确认系统模型是不是正确的,验证器通过搜索系统可以检查时钟约束和反应限制性质[13]。UPPAAL验证器使用快速搜索的方法检查系统的约束条件以及状态跳转,以避免搜索过程中的空间爆炸问题,其中验证器中的自动机语言(Backus Naur form,BNF)及含义见表1[14-15],其中:A表示“所有”,E表示“存在”,p表示“表达式”。
表1 BNF语法及含义
2.1 CTCS-3到CTCS-N等级转换场景分析
CTCS-3转换至CTCS-N的转换过程分为RBC切换和车载设备等级转换两部分,如图1所示,其中:RBC1表示CTCS-3区域内的RBC(简称C3-RBC),RBC2表示CTCS-N区域内的RBC(简称CN-RBC),CN-TSRS表示新型列控系统的TSRS。新型列控系统区域内的RBC与相邻的CTCS-3区域内的RBC应保持连接,以CTCS-3的协议和流程完成列车移交。
图1 CTCS-3转换至CTCS-N的示意图
当列车的行车许可终点到达RBC切换应答器时,C3-RBC发送预告信息给CN-RBC,并申请新型列控系统的进路信息;C3-RBC收到新型列控系统的进路信息后,则发送延长至CN-RBC区域内的行车许可到车载设备;列车安全前端经过TSRS呼叫应答器后,车载设备呼叫CN-TSRS,并且注册和下载CN-TSRS提供的行车许可;C3-RBC在列车靠近RBC切换应答器时发送RBC切换命令到车载设备;CN-RBC在列车安全前端越过RBC切换应答器后向C3-RBC发送接管信息,车载设备接收CN-RBC的等级转换命令和行车许可;列车安全后端越过RBC切换应答器后,车载设备中断与C3-RBC之间的通信;列车越过等级转换应答器时车载设备自动转入CTCS-N控车。信息交互顺序图如图2所示。
图2 CTCS-3转换至CTCS-N的信息交互图
2.2 CTCS-N到CTCS-3等级转换场景分析
CTCS-N转换至CTCS-3的转换过程(见图3)分为车载等级转换和RBC切换两部分。新型列控系统区域内的RBC与相邻的CTCS-3区域内的RBC应保持连接,以CTCS-3的协议和流程完成列车移交。
图3 CTCS-N转换至CTCS-3的示意图
当列车的行车许可终点到达RBC切换应答器组时,CN-RBC发送列车预告信息至C3-RBC,并且申请进路信息;CN-RBC收到C3-RBC发送的进路信息后,向车载设备发送延长至C3-RBC区域的行车许可;车载设备在列车越过等级转换应答器后,自动转换到CTCS-3控车;CN-RBC在接近RBC切换边界时向车载设备发送RBC切换命令,车载设备与C3-RBC建立通信;车载设备在列车前端越过RBC切换应答器后仅接收C3-RBC的行车许可;车载设备在列车后端越过RBC切换应答器后终止与CN-RBC的通信会话。信息交互顺序图如图4所示。
图4 CTCS-N转换至CTCS-3的信息交互图
2.3 故障模式下CTCS-3到CTCS-N等级转换场景分析
根据青藏铁路新型列控技术规范,CTCS-3转换至CTCS-N的过程中车载设备故障模式主要有两种。根据铁路信号“故障-安全”原则,即当信号设备发生故障后,应以特殊的方式做出反应并导向安全[16]。所以CTCS-3到CTCS-N等级转换场景在故障模式下导向安全有两种情况:
1) 列车安全前端越过RBC切换应答器后,车载设备未收到CN-RBC的期望消息,则车载设备仍按C3-RBC的行车许可行车,即列车降级运行,这样会影响行车效率。
2) 车载设备在移交RBC前仅与C3-RBC通信正常时,车载设备应该重新呼叫CN-RBC,并且完成列车注册和进路信息的申请。
等级转换场景的主要研究对象为车载设备、应答器、C3-RBC、CN-RBC、TSRS。
基于UPPAAL构建整个系统的TA模型:TA=Onboard‖Balise‖RBC1‖RBC2‖TSRS,其中:Onboard表示车载设备,Balise表示应答器。在系统模型中,各个子系统之间通过同步通道实现通信,其中:“!”表示发出此信号后转换发生,“?”表示接收此信号后转换发生。
设时间自动机的位置集合为L,则L=LOnboard∪LBalise∪LRBC1∪LRBC2∪LTSRS,其中:LOnboard、LBalise、LRBC1、LRBC2、LTSRS分别表示车载设备、应答器、RBC1、RBC2、TSRS的时间自动机模型的非空状态集。系统的状态位置集合如下所示:
LOnboard={idle,GetRBC2MA,ConnectCmd,StartConTSRS,Getversion_TSRS,Connectbuild_TSRS,…};
LBalise={idle,sendTSRSCall,sendRBCchange,sendLTO,sendLTA};
LRBC1={idle,ApplyInfo,RecRoute,GetRouteSuc,SendRBC2MA,ApprochRBC,SendRBCcmd,…};
LRBC2={idle,GetPreview,SendRoute,GetconRBC2,Sendversion_RBC2,Buildcnnect_RBC2,…};
LTSRS={idle,GetconTSRS,Sendversion_TSRS,Buildcnnect_TSRS,SendEM}。
等级转换场景中,应答器的时间自动机模型如图5所示,临时限速服务器的时间自动机模型如图6所示,车载设备的时间自动机模型如图7所示,CTCS-3区域内无线闭塞中心的时间自动机模型如图8所示,CTCS-N区域内无线闭塞中心的时间自动机模型如图9所示。
图5 Balise的时间自动机模型
图6 TSRS的时间自动机模型
图7 Onboard时间自动机模型
图8 RBC1的时间自动机模型
图9 RBC2的时间自动机模型
Onboard时间自动机模型中状态位置与变量的含义见表2。
表2 模型中关键位置与关键变量
Tab.2 Key positions and key variables in the model
4.1 模型仿真
时间自动机模型的仿真通过UPPAAL的模拟器生成消息顺序图来实现[17],用于保证模型的完整性与一致性。图10为模型输入到UPPAAL模拟器中的模型,图11为车载设备由CTCS-3等级转换到CTCS-N等级生成的消息顺序图,图12为车载设备由CTCS-N等级转换到CTCS-3等级的消息顺序图。
图10 模拟器中系统模型
图11 CTCS-3转换至CTCS-N的消息顺序图
图12 CTCS-N转换至CTCS-3的消息顺序图
4.2 模型验证
时间自动机模型的验证是通过UPPAAL的验证器进行验证的[18]。模型的验证主要是从系统的功能要求、性能要求和故障状态下的系统要求3个方面进行分析。基于表1所列的BNF范式进行模型验证,程序实体如下:
a.系统的功能要求
1) 系统无死锁:A[]not deadlock。
2) C3-RBC在行车许可终点到达RBC切换应答器时向CN-RBC发送列车预告信息并且申请进路信息。当收到CN-RBC的进路信息时,向车载设备发送CN-RBC区域的行车许可(CN-RBC在行车许可到达RBC切换应答器时向C3-RBC发送列车预告信息并申请进路信息;当收到C3-RBC的进路信息时,向车载设备发送C3-RBC区域的行车许可)。此功能的验证程序为:E<>((RBC1.idle imply RBC1.ApplyInfo) and (RBC1.idle imply RBC1.GetRouteSuc) and (RBC1.idle imply RBC1.SendRBC2MA)) and ((RBC2.idle imply RBC2.ApplyInfo) and (RBC2.idle imply RBC2.GetRouteSuc) and (RBC2.idle imply RBC2.SendRBC1MA))。
3) 车载设备根据应答器信息向TSRS发起会话。若车载设备收到TSRS发送的版本信息,则表明会话建立成功,接着下载电子地图。此功能的验证程序为:E<>((Onboard.idle imply Onboard.ConnectCmd) and (Onboard.idle imply Onboard.Connectbuild_TSRS) and (Onboard.idle imply Onboard.DownloadEM))。
4) CTCS-3转换至CTCS-N时,列车接近RBC转换应答器,C3-RBC向车载设备发送RBC切换命令。若车载通信电台正常则呼叫CN-RBC;若通信电台故障,则呼叫失败(CTCS-N转换至CTCS-3时,列车接近RBC转换应答器,CN-RBC向车载设备发送RBC切换命令。若车载通信电台正常,则呼叫C3-RBC;若通信电台故障,则呼叫失败)。此功能的验证程序为:E<>((RBC1.idle imply RBC1.ApprochRBC) and (RBC1.idle imply RBC1.SendRBCcmd) and (Onboard.idle imply Onboard.StartcomRBC2)) and ((RBC2.idle imply RBC2.ApprochRBC) and (RBC2.idle imply RBC2.sendRBCcmd) and (Onboard.idle imply Onboard.StartcomRBC1))。
5) CTCS-3转换至CTCS-N时,在移交列车控制权前,若车载设备仅与C3-RBC通信正常,则车载设备重新呼叫CN-RBC(CTCS-N转换至CTCS-3时,在移交列车控制权前,若车载设备仅与CN-RBC通信正常,则车载设备重新呼叫C3-RBC)。此功能的验证程序为:E<>((Onboard.idle imply Onboard.FailComRBC2) and (Onboard.idle imply Onboard.StartcomRBC2)) and ((Onboard.idle imply Onboard.FailComRBC1) and (Onboard.idle imply Onboard.StartcomRBC1))。
6) CTCS-3转换至CTCS-N时,车载设备在列车前端越过等级转换应答器后转换至CTCS-N等级(CTCS-N转换至CTCS-3时,车载设备在列车前端越过等级转换应答器后转换至CTSCS-3等级)。此功能的验证程序为:E<>(Onboard.idle imply Onboard.HeadpassLTO) and (Onboard.idle imply Onboard.ConversionCN) and ((Onboard.idle imply Onboard.PassLTA) and (Onboard.idle imply Onboard.ConversionC3))。
7) 等级转换场景中,CN-RBC应能接收CTCS-3级车载设备的位置报告,并发送相应的行车许可。此功能的验证程序为:E<>((RBC2.idle imply RBC2.Getloc) and (RBC2.idle imply RBC2.SendCCandMA))。
b.系统的性能要求
1) 车载设备呼叫RBC、TSRS的时间不应该大于20 s。此性能的验证程序为:A<>((Onboard.Connectbuild_TSRS imply Ttsrs<=20) and (Onboard.Connectbuild_RBC2 imply Trbc<=20) and (Onboard.Connectbuild_RBC1 imply Trbc<=20))。
2) 车载设备与RBC进行通信的时间不应该大于20 s。此性能的验证程序为:A<>(Onboard.GetCCandMA imply Tcom<=20)。
c.故障状态下的系统要求
1) CTCS-3转换至CTCS-N时,列车越过RBC切换应答器后,当车载设备未收到CN-RBC的消息时,车载设备降级运行。故障状态下系统的验证程序为:E<>((Onboard.Sendloc imply MA<1) and (Onboard.idle imply Onboard.FailConCN) and (Onboard.idle imply Onboard.InC3))。
2) CTCS-3转换至CTCS-N时,车载设备在移交RBC前,如果与CN-RBC通信中断,车载设备重新呼叫CN-RBC并且完成列车注册与进路信息的申请。故障状态下系统的验证程序为:E<>((Onboard.Connectbuild_RBC2 imply RBC_2<1) and (Onboard.idle imply Onboard.FailComRBC2) and (Onboard.idle imply Onboard.GetRBCcmd))。
将上述验证该系统需求的BNF语句输入到验证器中进行验证。在验证器中验证语句后面的绿色圆圈表示验证通过,红色表示不通过。验证结果如图13所示,可以看出,本文所建立的模型满足CTCS-N的需求。
图13 模型验证图
1) 基于技术规范分析了新型列控系统等级转换场景的具体流程,并且对该场景的车载设备、应答器、C3-RBC、CN-RBC、TSRS的信息交互进行了准确描述。然后提取功能需求,基于TA语言使用UPPAAL建立时间自动机模型。
2) 建立新型列控系统在该场景的时间自动机模型后,使用模拟器生成消息顺序图,用于仿真各个子模型之间的信息交互场景。通过仿真模型的通信过程可以使系统设备间信息交互的理解更加形象,并且可以检验出模型是否存在缺陷、错误,完善系统的设计。
3) 根据新型列控规范整理车载设备由CTCS-3转换至CTCS-N的主要故障模式,通过验证器对模型的正常和故障模式进行了验证,确保了所建模型的功能与性能满足技术规范。验证通过后,本文建立的时间自动机模型可以作为场景原型在系统功能测试阶段和故障分析时起到重要作用,有助于减少测试的投入。
猜你喜欢 自动机应答器控系统 {1，3，5}-{1，4，5}问题与邻居自动机数学物理学报(2021年3期)2021-07-19关于DALI灯控系统的问答精选家庭影院技术(2021年3期)2021-05-21联调联试中列控系统兼容性问题探讨铁道通信信号(2020年5期)2020-09-21应答器THR和TFFR分配及SIL等级探讨铁道通信信号(2020年9期)2020-02-06一种基于模糊细胞自动机的新型疏散模型智富时代(2019年4期)2019-06-01一种基于模糊细胞自动机的新型疏散模型智富时代(2019年4期)2019-06-01广义标准自动机及其商自动机西北大学学报（自然科学版）(2018年2期)2018-04-18一种新型列控系统方案探讨铁道通信信号(2016年10期)2016-06-01虚拟应答器测试方法研究铁道通信信号(2016年4期)2016-06-01应答器在基于通信的列车控制系统中的应用城市轨道交通研究(2015年11期)2015-02-27