CTCS-3级列控系统RBC控车场景建模与验证

CTCS-3级列控系统RBC控车场景建模与验证

CTCS-3级列控系统RBC控车场景建模与验证 CTCS-3级列控系统RBC控车场景建模与验证 盛昭君,米根锁 (兰州交通大学自动化与电气工程学院, 兰州 730070) 摘 要：应用统一建模语言UML与模型检验工具

PHAVer(Polyhedral Hybrid Automaton verifier)相结合的方法,研究CTCS-3级列控系统RBC控车场景：列车注册与启动、行车许可、等级转换、列车注销的混成性。首先通过UML支持的扩展机制,引入构造型(Stereotype)对UML进行面向混成性的扩展,建立RBC控车场景UML模型,实现对RBC控车场景混成性的描述。然后依据UML到PHAVer的转换规则,将UML模型转换成PHAVer模型。最后,依据CTCS-3级列控系统需求规范,总结RBC控车场景的功能需求,运用PHAVer进行验证,证明CTCS-3级列控系统需求规范的正确性。 关键词：CTCS-3级系统；RBC控车场景；UML；PHAVer RBC控车场景具有显著的混成性，CTCS-3级列控系统相关设备不仅要实时计算列车一些连续变量(如距离、速度、加速度等)的演化过程,还需考虑RBC控车场景中涉及到列车与驾驶员或者系统设备交互的离散事件,这两方面相互作用,共同影响系统的安全。因此,采用有效方法对RBC控车场景的混成性进行研究,不仅能够为CTCS-3级列

控系统研发提供参考,而且对保障列车的安全运行具有重要意义。 目前大多数文献仅从离散信息交互过程的角度分析列控系统,而没有考虑列车的连续动态过程。文献[1]基于实时系统模型检验工具UPPAAL,从RBC与其他外部设备信息交互的角度,对RBC系统的控车流程进行了建模与分析。文献[2-3]分别基于随机petri网和赋时着色petri网,将GSM-R故障模型和消息模型作为底层模型,对CTCS-3级RBC系统控车场景进行了建模与分析。 因此,本文通过对UML进行面向混成性的扩展,建立RBC控车场景UML模型,采用模型检验工具PHAVer,对RBC控车场景的混成性进行验证。 1 RBC控车场景 本文对CTCS-3级列控系统RBC控车场景[4-6]：列车注册与启动、行车许可、列车注销和等级转换进行建模与验证。 假定线路区间由s[0]，s[i],…，s[14]共15个闭塞分区组成。s[7]与s[8]边界为CTCS-3级控制单元转CTCS-2级控制单元边界；s[11]与s[12]边界为CTCS-2级控制单元转CTCS-3级控制单元边界。每个闭塞分区布置1个Balise,向OBE发送列车位置信息s,对SDU测得的列车位置进行矫正；在特殊位置(如等级转换预告点、执行点等)向OBE发送相关命令。仅取一辆列车的运行过程进行研究。 2 RBC控车场景UML模型 针对RBC控车场景混成性建模,需通过带有连续变量的微分表达式刻画系统中连续的物理过程以及保持这些过程的微分动态约束条件；以不变集或信号事件等

为条件的状态迁移刻画离散变化过程。因此,需通过UML支持的扩展机制[7-8],引入构造型(Stereotype),对UML进行扩展,建立针对RBC控车场景混成性的UML模型。 表2 图1中各类触发事件的含义消息含义消息含义Msg100车载请求与RBC建立连接Msg42RBC向车载发送终止通信会话Msg3C3系统配置参数Msg155车载向RBC发送“通信会话开始”消息Msg8列车数据确认信息Msg154车载向RBC发送终止通信会晤(未建)Msg159通信会话已建立报告Msg41级间转换命令Msg136列车位置报告Msg39通信会晤结束确认消息Msg129列车数据信息infchoosegrade通知司机选择列控系统等级Msg132请求MADriveoff列车停车，通知司机关闭驾驶台Msg156列车结束通信会话(已建)CTCSgradeconfirm司机对CTCS控制单元进行确认Msg147CEM确认消息SB常用制动命令Msg150任务结束消息EB紧急制动命令Msg44MA回复消息relEB紧急制动缓解Msg32系统配置信息SMARBC向车载发送的缩短MA消息Msg57位置报告参数CEMRBC向车载发送的有条件紧急停车消息Msg58行车许可请求UEMRBC向车载发送的无条件紧急停车消息Msg34确定前方轨道空闲SBbad常用制动故障closeOBE关闭车载设备电源informcom通知司机通信会话已建立SDU＿s实测距离speedmeasure速度测量Balise＿s应答器位置driconfirm司机对列车行车进行确认

update＿s更新列车位置leave列车离开闭塞分区update＿v更新列车速度enter列车进入闭塞分区acc/dec列车加速/减速过程Locunconsistent位置未知，选择C2passRN列车最小安全末端通过边界Safeconnect通知司机安全连接已建立GotoC2/C3通知司机选择工作等级relSB常用制动缓解conconfirm司机对连接进行确认SDU＿v实测速度depconfirm司机对列车发车进行确认distncemeasure距离测量Informdepart通知司机发车Informdrive通知司机行车send＿vSDU向OBE发送列车速度 2.1 RBC控车场景UML类图 将RBC控车场景相关设备抽象为测速测距单元(SDU)、应答器(Balise)、Driver、列控中心(TCC)、RBC、OBE和Train,构成UML类图中7个相互关联的类，UML类图,如图1所示。图1中每个类的属性见表1,触发事件的含义见表2。 图1 RBC控车场景UML类图 表1 图1中各类属性的含义变量类型变量及含义连续变量s，pos，epos，rpos均表示列车的位置v表示列车的速度t表示时间变量，dt=1离散变量a表示列车的加速度(Amax表示最大值)bs表示列车的常用制动减速度be表示列车的紧急制动减速度vp表示列车的允许速度s[i]，m[i]均表示第i个闭塞分区的状态eoa表示MA的终点位置vr表示MA的顶棚限制速度T，vmax均表示常量ve，de均表示列车计算目标距离监控变量d表示闭塞分区长度vEBI表示紧急制动速度触发值vSBI表示常用制

动速度触发值 2.2 RBC控车场景UML顺序图 UML顺序图由RBC注册与启动场景(内含行车许可场景)，RBC注销场景，CTCS-2级转CTCS-3级场景，CTCS-3级转CTCS-2级场景以及Train运行过程5部分组成。其中，Train运行过程UML顺序图,如图2所示。 图2 Train运行过程的UML顺序图 RBC初始条件：区段状态m[i]=0，i≤14,列车位置rpos=0，eoa=0,区段限速vr=0。RBC将从OBE收到的位置信息epos赋值给rpos,将从TCC收到的区段状态信息s[i]赋值给m[i],由此可以求得MA的终点位置,其计算公式如下 赋值最大速度vr=vmax,并将(eoa，vr)发送给OBE。当列车速度v达到180 km/h时，RBC向OBE发送SMA信息；当列车位置进入第4个闭塞分区时，RBC向OBE发送CEM信息；当列车位置进入第5个闭塞分区时，RBC向OBE发送UEM信息。 列车初始条件：v=0，a=0，s=0,初始位置占用股道为i=0,列车位置epos=0,目标速度ve=0,与eoa之间的距离de=0,列车的允许速度vp=0,列车紧急制动a=be,周期T=1。当OBE收到SDU发送的列车速度v后,计算列车位置 并被Balise发送的位置s矫正epos=s,当从RBC收到信息(eoa，vr)后,可以求得与eoa之间的距离de,列车目标速度ve,列车允许速度vp,紧急制动速度触发值vEBI,常用制动速度触发值vSBI,其计算公式分别如下式 2.3 RBC控车场景UML状态图 UML状态图由RBC、OBE、