基于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.