基于HUML的列控系统形式化建模与参数分析方法

赵晓宇 , 程瑞军, 程 雨, 马小平,4

(1. 中国铁道科学研究院 研究生部，北京 100081； 2. 北京交通大学 轨道交通控制与安全国家重点实验室， 北京 100044；3. 中国铁道科学研究院 基础设施检测研究所，北京 100081； 4. 北京交通大学 交通运输学院，北京 100044)

列车运行控制系统既包含连续的运行过程，又包含有离散的控制行为，属于典型的混成系统[1]。各国学者采用不同的形式化方法研究了列控系统的混杂性[2-6]，但均未讨论过含有未知控制参数的混成模型。然而，在系统开发的初始阶段，如何根据系统的安全性需求分析得到系统控制参数之间所满足的约束集，对系统安全显得尤为重要。因此，本文针对高速铁路列控系统，提出一种基于混成统一化建模语言HUML(Hybrid Unified Modeling Language)的列控系统形式化建模与参数分析方法。通过定义HUML到HYTECH模型的转换规则，将HUML模型转换成HYTECH，并运用模型检验工具HYTECH对模型的状态可达性进行验证。然后将安全性需求加入到满足可达性验证的模型，建立安全HYTECH模型，通过计算该模型的可达集，得到未知控制参数所需满足的约束集。最后，以移动闭塞中的追踪模型为例，采用该方法对列车的距离控制器进行建模和分析。通过分析得到控制参数的取值范围，对所得参数的验证结果表明该方法的有效性。

1 基于HUML模型的控制参数分析方法

基于HUML模型的控制参数分析方法基本流程见图1。具体步骤为：

Step1根据系统的需求规范或者协议文件，通过合理抽象并运用混成UML概要文件，建立系统的模型。所建立的抽象模型可能含有未知参数变量，转化过程必须满足转换的一致性。定义由HUML模型到HYTECH模型的转换规则。

Step2根据HUML模型到HYTECH模型的转换规则，将HUML模型转换为HYTECH抽象可执行模型。定义模型的初始状态，并对HYTECH模型进行可达性分析，以判定该模型的所有状态(不包括危险状态)是否具有可达性属性。当模型不满足状态可达性时，需要对模型进行修改，直到满足可达性为止。当满足可达性后，可以进入到下一步的分析。

Step3将系统的安全性需求定义为Final_region，则新模型中包含了与安全性相关的指标。对新建立的HYTECH模型进行可达性分析，计算系统所含未知控制参数需要满足的约束不等式集合。当参数取值满足该约束集时，模型将满足安全性需求，否则不满足安全性需求，需修改控制模型。

Step4选择满足所得约束集的系统控制参数建立具体的HYTECH模型，通过分析有界时间内模型的所有可执行路径，修正模型的控制参数的取值，直到得到满意的控制参数为止。

1.1 建立HUML模型

规范是系统开发的起点和基础，而系统需求规范一般以自然语言的形式描述，自然语言存在歧义性将不利于需求规范的验证。统一化建模语言(UML)作为半形式化的建模语言，提供了一系列的扩展机制，满足了特定领域建模的需要。UML的扩展机制[7-9]主要包括：构造型(Stereotype)、标记值(Tagged Value)和约束(Constraint)，本文主要采用构造型的扩展方法。

为刻画列控系统所具有的混成特性，运用混成自动机对需求规范进行建模。设计的HUML概要文件主要有数据类型概要文件(Datatype Profile)、类概要文件(Class Profile)、约束和表达式概要文件(Expression and Constraint Profile)和状态机概要文件(Statemachine Profile)。以下主要说明扩展状态机概要文件。

扩展状态机定义状态与对应的表达式和约束之间的关系，以及状态之间的迁移关系。扩展状态机概要文件可以包含状态(State)、迁移条件(Transition)、区域(Region)、活动(Activity)等元素的扩展，具体的扩展元素根据实际需要进行选取。本文主要对混成自动机的状态(State)、状态内部包含的流条件(FlowCondition)、不等式条件(InvariantCondition) 和迁移条件(Transition)进行了扩展。其中，ModeState对元类State进行了扩展。见图2，扩展状态概要文件描述了扩展状态(ModeState)与表达式(Expression)和约束(Constraint)之间的关系。其中，Stereotype 表示构造型，metaclass表示UML已经定义的元类元素。构造型ModeState具有Constraint和Expression两种属性。Expression(约束)有InvExpression(状态变量满足的不等式约束)和stateFlow(状态变量微分满足的约束)两种形式。 iniState{subsets ownedRule}表示初始状态(iniState)具有的属性。

1.2 由HUML模型到HYTECH模型的转换规则

根据HYTECH模型的结构定义[10]，将扩展后建立的HUML模型转化为HYTECH形式化模型，主要有以下方面：

(1) 系统组成

HYTECH模型由个或多个自动机模块(Automaton)和系统分析操作指令两部分组成。自动机模块描述系统所有包含的离散状态(Location)，各离散状态之间的迁移过程，以及离散状态内部的连续变化过程。HYTECH模型中系统分析操作命令部分包括region变量的声明(包括initial region和final region)、系统的组成结构及根据模型分析的类型声明不同的分析操作指令。在进行安全分析时，final region一般为危险状态集，initial region为系统的初始状态集。根据不同的分析目的编写分析操作指令模块部分。

(2) 自动机模块

HYTECH模型中的自动机模块对应HUML的扩展类(《Agent》)和扩展状态机中的状态(《Mode State》)，包含系统的静态属性及动态行为描述。每个自动机包含有一个或者多个状态(loc)，以及所有离散状态之间的迁移(Transition)。每个location包含有对应离散状态的invariant condition和flow condition描述。完整的自动机模块由变量声明(var)、标签定义(synclabs)、状态描述(loc)以及迁移过程(transition)的定义等几部分组成。

(3) 系统变量声明

离散状态(loc)的连续变量类型有模拟型(analog)，时钟型(clock)，计时类型(stopwatch)等，其中clock的变化率为1，stopwatch的变化率或为0或为1，analog类型变量的变化率没有限制。离散控制变量对应discrete类型变量，其变化率为0。待确定的参数值为parameter类型的变量，其变化率为0且不能进行赋值，以及常量(由define 语句进行定义)的声明。

(4) 标签定义

标签定义以关键字synclabs作为标记。该标签的定义主要是用于同步各自动机的共享事件，尤其在并发分布式系统中具有重要的作用。对应于HUML模型中的迁移触发事件。

(5) 状态描述

在离散状态loc中，flow condition对应于wait关键词所标记的内容，用于描述状态loc所包含变量的变化率，一般是由区间或常量表示。invariant condition对应于while关键词标记的内容，描述状态所含变量须满足的不等式约束集。

(6) 迁移过程的定义

迁移过程的具体定义以关键字when开始。每1迁移对应于1条when…do…goto语句。loc关键词标记对应迁移的源状态(source location)，when关键词后是对应迁移的迁移卫式(guard)，do关键词后是对应迁移的置位表达式(reset)，goto关键词后是对应迁移的目标状态(target location)。当守卫条件无约束时，guard为True。发生迁移后变量的值保持不变，则reset可以表示为v′=v(v′表示变量v的下一状态，v表示变量v的当前状态)。发生迁移后，变量的值不确定表示为x′=x。

(7)系统分析操作指令模块

分析操作指令部分包括region变量的声明(包括initial region和final region)，系统的组成结构，以及根据模型分析的不同目的声明不同的分析操作指令。在进行安全分析时，final region一般为危险状态集，用于描述系统最终所处的状态，对应于系统的安全性需求的形式化描述。initial region定义了组成系统的自动机组合和各自动机中的变量所满足的初始状态集，对应于HUML所包含的扩展类Agent和各自动机的初始状态集(Initial Constraint)。

1.3 混成自动机模型中未知控制参数的分析

HYTECH模型通过计算系统的可达集分析系统模型的未知参数。可达集的计算有前向可达集计算和后向可达集计算两种。‘reach forward from 〈reg_exp〉 endreach’用于表示前向可达集计算的操作指令，其中reg_exp表示系统的初始状态集合。当final_region与可达集的交集为空时，表示满足系统的安全性需求。否则，模型不满足安全性需求。‘reach backward from〈reg_exp〉 endreach’表示后向可达集计算指令，其中reg_exp一般为final_reg，在安全分析中，final_reg一般表示危险状态集合。通过不断向前迭代的方式，当final_reg的可达集与initial_reg的交集为空时，表示满足系统的安全性需求。否则，不满足安全性需求。

2 案例分析

2.1 场景描述

传统的信号控制系统是基于固定闭塞的控制系统，未考虑列车的不同速度和制动性能，闭塞区间的长度固定不变，这影响轨道的利用效率。移动闭塞取消了固定的闭塞区间划分，闭塞区间间隔随列车的运行动态变化，降低了列车运行间隔时间，提高了轨道的利用效率。移动闭塞追踪模型见图3，图3中包含的要素有列车定位(Train Position)、安全距离(Safety Distance)和目标点(Target Point)。其中，安全距离是列车实施最大常用制动的附加距离，保证列车在最坏的情况下列车不发生追尾，用图3中的SD表示。目标点是列车当前时刻能够运行到的最远点，相当于列车的移动授权。

在图3中横坐标表示列车运行的位置，纵坐标表

示后行列车在各位置点所对应的速度，SBI表示最大常用制动曲线，EBI表示紧急制动曲线，SD表示安全距离，EOA_SB和EOA_EB分别表示常用制动曲线和紧急制动曲线的终点，REL表示列车的缓解速度曲线，SBD表示列车开始实施制动时的位置点。

2.2 建立移动闭塞追踪模型的线性混成自动机模型

在实际的运营过程中，某区段中有多辆列车同时运行，为简便起见，该模型仅考虑两辆列车单向追踪的场景。根据移动闭塞系统工作原理，建立后行列车的距离控制器的线性混成自动机模型，见图4。由于该模型中包含有未知控制参数，因此属于抽象混成自动机模型。并假定前行列车为匀速行驶，后行列车实施制动(紧急制动或常用制动)时的加速度为恒定值，即不考虑列车加速和实施制动时达到最大加速度和最大制动能力所需的延迟时间。在该模型中，不考虑列车的制动距离，仅考虑两列车之间的安全防护距离，取为400 m。相邻列车的追踪间隔由距离控制器控制，确保两车的间隔不小于400 m，从而保证两车不发生追尾事故。该控制器连续不断与无线闭塞中心RBC保持通信，接收列车的位置和速度信息，并通过计算得到两车间的距离。后行列车最大速度vmax为220 km/h，最小速度为0。运用Δ表示从RBC接收到的2个MA信息的时间间隔，因此，不再考虑移动闭塞系统中不同模块间的交互过程。

距离控制器模型包含有7个状态：idle(静止), acc(加速), max_speed(最大速度运行), eb(紧急制动), sb(常用制动), release(缓解制动)和crash(危险状态)。模型中，x表示两相邻列车之间的距离间隔。xf,vf和af分别表示后行列车的前端位置，速度和加速度值。xl,vl和al分别表示前行列车的尾部位置，速度和加速度值(本文中位置、速度和加速度的单位分别为m、km/h和m/s2，以下同)。参数D_eb，D_sb，D_rele和D_acc表示该控制模型的控制参数，当列车间隔达到对应的值时，将会触发状态相应的迁移。在迁移过程中，位置(xf、xl)和速度(vf、vl)的值不能被重置，根据所进入的状态，加速度af的值可以被重置。

模型中各状态对应的不等式约束和流条件为：除crash(危险状态)之外，其他所有所有状态都满足的不等式约束为：‘(x=xl-xf)∧(xf≥0)∧(xl≥0)∧(vl=140)∧(al=0)∧(Δ=3)’。所有状态满足的流条件为：‘(dx=dxl-dxf)∧(dxf=39)∧(dvl=0)∧(dal=0)’，其中dx,dv,da分别表示列车的位置、速度和加速度的变化率。

图4中各状态所对应的不等式条件Inv和对应的流条件Flow分别为

( 1 )

( 2 )

模型的迁移条件有迁移卫式和置位条件两种表达式。例如，x=D_eb表示的是迁移卫式，a:=-25为置位条件表达式。

列车的运动过程简述如下：初始时刻，后行列车可能处于静止或以最大速度运行。当列车之间的间隔大于零且小于D_eb时，列车实施紧急制动；当间隔大于D_eb且小于D_sb时，列车实施常用制动；当间隔小于0时，列车进入crash(危险状态)。紧急制动只有在列车停车后才能缓解，在两车的间隔大于D_rele时，可以缓解常用制动。当列车间的间隔大于D_acc时，后行列车将进入加速状态。所有控制参数的取值或取值范围不仅取决于列车的加速和制动性能，而且还与系统规定的安全性需求有关。

2.3 模型的转换及参数分析过程2.3.1 转换后的HYTECH模型片段

根据上述提出的转换规则，将HUML模型转换为可执行的HYTECH模型，控制器的HYTECH模型片段见表1。为了保证模型本身的正确性，首先需要验证模型的可达性，即当初始域(系统的初始状态满足的约束集)包括所有可能的初始状态时，控制器的所有状态(除危险状态外)必须为可达。若存在不可达状态，则表明该模型不完整需要修改模型。其次，根据系统的安全性需求，计算未知控制参数的约束集。为了说明所提出方法的有效性，以下首先对模型的可达集进行计算，然后给出控制参数约束集的生成过程。

表1 HYTECH模型片段

2.3.2 验证抽象HYTECH模型状态的可达性

根据提出的转换规则，将HUML模型转换为HYTECH模型，验证HYTECH模型的可达性。当追踪列车初始时刻处于idle状态且列车之间的距离区间为[800 m，3 000 m](即初始域：initial_region={loc[sys]=idle&x>800 &x≤3 000})，追踪列车的加速和制动性能见图4距离控制器模型所示，系统所含控制参数须满足的约束可根据实际情况决定。为方便分析规定未知参数所满足的约束不等式为‘(200≤D_eb≤D_sb≤D_rele≤D_acc)’。

对于该初始域及参数约束，计算得到可达状态集为StateSet={idle,acc,max_speed, sb,eb,release}，可达状态对应的可达集如下：

State=idle，ReachSet={x≤xl&x>800}；

State=acc，ReachSet={x≤xl&3x<=70vf+3D_acc&D_acc≤x&70vf+3D_acc≤3xl+12 600&D_acc>800}||{D_eb800}；

State=max_speed，ReachSet={D_sb8 800&xxl&x≤D_acc&D_acc>800}||{3x≤3D_acc+15 400&x≤xl&3D_sb<3x&3xl≥3D_acc+2 800&21x+12xl≥33D_acc+11 200&D_acc>800}||{D_sb800&53D_rele21x+12xl+20D_sb&D_eb

State=sb，ReachSet={x≤xl&x≤D_rele&x+14vf≤D_sb+3 080&D_eb800&8vf8 800}；

State=eb，ReachSet={7x+4xl>8 800&0800&x≤xl}；

State=release，ReachSet={x≤xl&x≤D_acc&D_rele800}；

为简洁起见，以上所列出的约束表达式中略去该状态初始定义时所满足的约束表达式，仅列出满足安全需求性指标时的可达集约束。当模型的可达集中包含有不允许出现的状态(列车追尾、超速或其他危险状态)时，需要对模型的控制参数进行修正，直到可达状态集中不包含危险状态为止。只有在保证模型满足可达性的前提下才能对参数进行分析。由StateSet结果可见，该模型可达集中不包含crash状态且其他状态都可达，因此该模型满足可达性的基本属性，可以进行下一步的分析。

2.3.3 控制参数约束集的计算

在保证可达性属性后，计算满足安全性需求的控制参数约束集。初始域(Initial_reg)表示系统对应的初始状态及状态约束集。目标集(Final_reg)表示控制器的禁止状态，其中‘loc[sys]=crash’表示相邻的列车发生碰撞，‘x≤400’表示列车间隔低于400 m，‘x≥7 000’表示列车间隔大于7 000 m。其中，‘x≤400’是为了保证安全需求，而‘x≥7 000’是为了保证轨道的利用效率。控制参数约束集(ConstraintSet)的意义是：当系统初始状态满足初始域时，为了使系统不处于目标集状态，所有的控制参数必须满足的不等式约束。也即控制参数满足约束集ConstraintSet时，不仅可以保证系统为安全，同时能够提高轨道的利用效率。追踪列车的加速和制动性能如模型中所示。目标集定义为：列车之间的距离大于400 m小于7 000 m且两车不发生追尾，即Final_region={x≥7 000∨x≤400&vf>0∨loc[sys]=crash}。下面分析不同的初始状态和安全性指标，控制参数须满足的约束集，其中IRi表示系统的初始状态，CSi表示对应参数的约束集合。

(1) 初始时列车处于idle状态，与前行列车距离区间为[800，3 000]，运行速度为0。

IR1={(Loc[sys]=idle)&(x≥800)&(x≤3 000)&(vf=0)&(af=0)&(xl>xf)}，CS1={(D_sb≥400∨D_acc≤800)&(D_acc<800∨D_eb≥400∨D_acc1 005)&(D_eb≤800)}

(2) 初始时列车处于max_speed状态且与前行列车距离区间为[800，3 000]，运行速度为220 km/h。

IR2={(Loc[sys]=max_speed)&(x≥800)&(x≤3 000)&(vf=220)&(af=0)&(xl>xf)}，CS2={(D_sb≥400)}

(3) 初始时列车处于acc状态，与前行列车距离区间为[3 000，6 000]，运行速度为180 km/h，加速度1.67 m/s2。

IR3={(Loc[sys]=acc)&(x≥3 000)&(x≤6 000)&(vf=180)&(af=6)&(xl>xf)}，CS3={(D_sb≥400)&(3D_rele<8 500∨D_rele>3 000)}

(4) 初始时列车处于idle状态，与前行列车距离区间为[3 000，6 000]，运行速度为0。

IR4={(Loc[sys]=idle)&(x≥400)&(x≤3 000)&(vf=0)&(af=0)&(xl>xf)}，CS4={(D_acc≤400∨D_sb≥400)&(D_acc≤400∨D_eb≥400∨D_acc≥884)&(D_eb≤400)}

(5) 初始时列车处于acc状态，运行速度为200 km/h，与前行列车距离区间为[300，6 000]，加速度为1.67 m/s2。

IR5={(Loc[sys]=acc)&(x≥3 000)&(x≤6 000)&(vf=200)&(af=6)&(xl>xf)}，CS5={(D_sb≥400)&(3D_rele≤8 780∨D_rele>3 000)}

对于具有不同性能的列车满足相同安全需求(Final_reg={loc[sys]=crash∨x≥7 000∨x≤400})的情况，可以根据列车性能计算得到不同的控制参数约束集，从而实现控制模型的重用。Initial_reg和Final_reg分别表示初始域和目标域，ParaConsSet表示控制参数约束集。下面分别对3种性能的列车进行分析，分析结果为:

(1) 列车的加速度为4 m/s2，常用制动减速度为-8 m/s2，紧急制动减速度为-15 m/s2。

Initial_reg1={(Loc[sys]=idle)&(x≥800)&(x≤3 000)&(vf=0)&(af=0)&(xl>xf)}

ParaConsSet1={(D_sb≥400∨D_acc<800)&(D_acc<800∨D_acc>1 005∨D_eb≥400)}

(2) 列车的加速度为8 m/s2，常用制动减速度为-10 m/s2，紧急制动减速度-20 m/s2。

Initial_reg2={(Loc[sys]=acc)&(x≥800)&(x≤3 000)&(vf≥0)&(af=0)&(xl>xf)}

ParaConsSet2={(D_sb≥400∨D_acc<800)&(D_acc>884∨D_eb≥400∨D_acc<800)}

(3) 列车的加速度为6 m/s2，常用制动减速度为-8 m/s2，紧急制动减速度为-12 m/s2。

Initial_reg3={(Loc[sys]=acc)&(x≥800)&(x≤3 000)&(vf≥0)&(af=0)&(xl>xf)}

ParaConsSet3={(D_sb≥400∨D_acc<800)&(3D_rele>24 103∨D_rele<2 400)&(D_acc<800∨D_acc>1 005∨D_eb≥400)}

2.3.4 控制参数约束集验证

为证明所得控制参数约束的正确性，以下对约束集进行验证。当指定模型的控制参数值时，可以计算两车距离的区间范围。由上述分析结果知，系统初始域定义为

Initial_reg=(Loc[sys]=idle)&(xl>xf)&(x≥800)&(x≤3 000)&(vf=0)&(af=0)时，由安全需求定义系统的目标集为Final_reg=loc[sys]=crash∨x≥7 000∨x≤400，计算得到参数约束集为ConstraintSet=(D_sb≥400∨D_acc≤800)&(D_eb≤800)&(D_acc≤800∨D_eb≥400∨D_acc>884)。考虑到初始约束200≤D_eb≤D_sb≤D_rele≤D_acc≤3 000。因此，控制参数取为：D_eb=400,D_sb=500,D_rele=700,D_acc=850”，根据这组控制参数计算列车间隔的区间。用distancemin和distancemax分别表示距离的最小值和最大值，它们都表示恒定不变的符号常量，将其引入到Final_reg，Final_reg={loc[sys]=crash∨x≤distancemin∨x≥distancemax}，然后进行可达性分析。当状态acc，eb，sb处的加速度值分别为4、-15、-8 m/s2时，对应的输出结果为distancemax≥2 295,distancemin>500 m。由该结果知，两列车的最大距离间隔为2 295 m，最小距离间隔为500 m。因而，当控制参数满足‘(D_sb≥400∨D_acc≤800)&(D_acc≤800∨D_eb≥400∨D_acc>884)&(D_eb≤800)’时，追踪列车之间的距离区间为[500,2 295]，该区间包含于[400,7 000]，即所选控制参数满足对应的安全性需求。

3 结束语

本文针对混成系统模型，在满足安全性需求的前提下，为推导线性混成自动机模型中未知控制参数之间所须满足的约束不等式，提出了未知参数分析方法。运用该方法可求解与安全性需求对应的参数约束集，从而保证控制系统的安全运行。最后以移动闭塞中的追踪模型为例，建立追踪模型控制器对应的HUML模型，运用所提出的方法对其进行分析，得到距离控制参数的约束集，并对所得到的参数结果进行验证。验证结果表明，得到的参数约束集能够满足系统的安全性需求。对于在线路上运行的性能不同的列车，可根据列车的性能参数生成不同的控制参数模型，实现控制模型的复用。

参考文献：

[1] HENZINGER T A. The Theory of Hybrid Automata[C]//Proceedings of the 11thIEEE Symposium on Logic in Computer Science. New York: IEEE, 1996: 278-292.

[2] FRANZLE M, HERDE C. HySAT: An Efficient Proof Engine for Bounded Model Checking of Hybrid Systems[J]. Formal Methods in System Design. 2007, 30(3): 179-198.

[3] BAIL L J, ALLA H, DAVID R. Hybrid Petri Nets[C]// Proceedings of the 1stInternational European Control Conference. Grenoble: EUCA, 1991: 1 472-1 477.

[4] HENZINGER T A, KOPKE P W, PURI A, et al. What's Decidable About Hybrid Automata[C]// Proceedings of the 27thAnnual ACM Symposium on Theory of Computing. New York: ACM, 1995: 373-382.

[5] PLATZER A. Differential Dynamic Logic for Hybrid Systems[J]. Journal of Automated Reasoning, 2008, 41(2):143-189.

[6] 吕继东, 李开成, 唐涛,等. 基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法[J].中国铁道科学,2012.33(5): 91-97.

LÜ Jidong, LI Kaicheng, TANG Tao,et al. Formal Modeling and Verification Method for High Speed Train Control System Based on Hybrid Communicating Sequential Process[J].China Railway Science, 2012,33 (5):91-97.

[7] Object Management Group.Unied Modeling Language: Superstructure Version2.0[EB/OL]. http: //www.omg.org/docs/formal/09-02-02.pdf, 2009.

[8] Object Management Group. A UML Profile for MARTE: Modeling and Analysis of Real Time EmbeddedSystems[EB/OL]. http://www.omg.org/spec/MARTE/1.1, 2011.

[9] BERKENKÖTTER K, BiSANZ S, HANNEMANN U, et al. The HybridUML Profile for UML 2.0.[J]. International Journal on Software Tools for Technology Transfer, 2006, 8(2): 167-176.

[10] HENZINGERT A, HO P H , WONG-Toi H. HyTech: The Next Generation[C]//Proceedings of the 16th Annual Real-time Systems Symposium. New York: IEEE, 1995: 56-65.