趙曉宇 , 程瑞軍, 程 雨, 馬小平,4

(1. 中國(guó)鐵道科學(xué)研究院 研究生部，北京 100081； 2. 北京交通大學(xué) 軌道交通控制與安全國(guó)家重點(diǎn)實(shí)驗(yàn)室， 北京 100044；3. 中國(guó)鐵道科學(xué)研究院 基礎(chǔ)設(shè)施檢測(cè)研究所，北京 100081； 4. 北京交通大學(xué) 交通運(yùn)輸學(xué)院，北京 100044)

列車運(yùn)行控制系統(tǒng)既包含連續(xù)的運(yùn)行過(guò)程，又包含有離散的控制行為，屬于典型的混成系統(tǒng)[1]。各國(guó)學(xué)者采用不同的形式化方法研究了列控系統(tǒng)的混雜性[2-6]，但均未討論過(guò)含有未知控制參數(shù)的混成模型。然而，在系統(tǒng)開發(fā)的初始階段，如何根據(jù)系統(tǒng)的安全性需求分析得到系統(tǒng)控制參數(shù)之間所滿足的約束集，對(duì)系統(tǒng)安全顯得尤為重要。因此，本文針對(duì)高速鐵路列控系統(tǒng)，提出一種基于混成統(tǒng)一化建模語(yǔ)言HUML(Hybrid Unified Modeling Language)的列控系統(tǒng)形式化建模與參數(shù)分析方法。通過(guò)定義HUML到HYTECH模型的轉(zhuǎn)換規(guī)則，將HUML模型轉(zhuǎn)換成HYTECH，并運(yùn)用模型檢驗(yàn)工具HYTECH對(duì)模型的狀態(tài)可達(dá)性進(jìn)行驗(yàn)證。然后將安全性需求加入到滿足可達(dá)性驗(yàn)證的模型，建立安全HYTECH模型，通過(guò)計(jì)算該模型的可達(dá)集，得到未知控制參數(shù)所需滿足的約束集。最后，以移動(dòng)閉塞中的追蹤模型為例，采用該方法對(duì)列車的距離控制器進(jìn)行建模和分析。通過(guò)分析得到控制參數(shù)的取值范圍，對(duì)所得參數(shù)的驗(yàn)證結(jié)果表明該方法的有效性。

1 基于HUML模型的控制參數(shù)分析方法

基于HUML模型的控制參數(shù)分析方法基本流程見圖1。具體步驟為：

Step1根據(jù)系統(tǒng)的需求規(guī)范或者協(xié)議文件，通過(guò)合理抽象并運(yùn)用混成UML概要文件，建立系統(tǒng)的模型。所建立的抽象模型可能含有未知參數(shù)變量，轉(zhuǎn)化過(guò)程必須滿足轉(zhuǎn)換的一致性。定義由HUML模型到HYTECH模型的轉(zhuǎn)換規(guī)則。

Step2根據(jù)HUML模型到HYTECH模型的轉(zhuǎn)換規(guī)則，將HUML模型轉(zhuǎn)換為HYTECH抽象可執(zhí)行模型。定義模型的初始狀態(tài)，并對(duì)HYTECH模型進(jìn)行可達(dá)性分析，以判定該模型的所有狀態(tài)(不包括危險(xiǎn)狀態(tài))是否具有可達(dá)性屬性。當(dāng)模型不滿足狀態(tài)可達(dá)性時(shí)，需要對(duì)模型進(jìn)行修改，直到滿足可達(dá)性為止。當(dāng)滿足可達(dá)性后，可以進(jìn)入到下一步的分析。

Step3將系統(tǒng)的安全性需求定義為Final_region，則新模型中包含了與安全性相關(guān)的指標(biāo)。對(duì)新建立的HYTECH模型進(jìn)行可達(dá)性分析，計(jì)算系統(tǒng)所含未知控制參數(shù)需要滿足的約束不等式集合。當(dāng)參數(shù)取值滿足該約束集時(shí)，模型將滿足安全性需求，否則不滿足安全性需求，需修改控制模型。

Step4選擇滿足所得約束集的系統(tǒng)控制參數(shù)建立具體的HYTECH模型，通過(guò)分析有界時(shí)間內(nèi)模型的所有可執(zhí)行路徑，修正模型的控制參數(shù)的取值，直到得到滿意的控制參數(shù)為止。

1.1 建立HUML模型

規(guī)范是系統(tǒng)開發(fā)的起點(diǎn)和基礎(chǔ)，而系統(tǒng)需求規(guī)范一般以自然語(yǔ)言的形式描述，自然語(yǔ)言存在歧義性將不利于需求規(guī)范的驗(yàn)證。統(tǒng)一化建模語(yǔ)言(UML)作為半形式化的建模語(yǔ)言，提供了一系列的擴(kuò)展機(jī)制，滿足了特定領(lǐng)域建模的需要。UML的擴(kuò)展機(jī)制[7-9]主要包括：構(gòu)造型(Stereotype)、標(biāo)記值(Tagged Value)和約束(Constraint)，本文主要采用構(gòu)造型的擴(kuò)展方法。

為刻畫列控系統(tǒng)所具有的混成特性，運(yùn)用混成自動(dòng)機(jī)對(duì)需求規(guī)范進(jìn)行建模。設(shè)計(jì)的HUML概要文件主要有數(shù)據(jù)類型概要文件(Datatype Profile)、類概要文件(Class Profile)、約束和表達(dá)式概要文件(Expression and Constraint Profile)和狀態(tài)機(jī)概要文件(Statemachine Profile)。以下主要說(shuō)明擴(kuò)展?fàn)顟B(tài)機(jī)概要文件。

擴(kuò)展?fàn)顟B(tài)機(jī)定義狀態(tài)與對(duì)應(yīng)的表達(dá)式和約束之間的關(guān)系，以及狀態(tài)之間的遷移關(guān)系。擴(kuò)展?fàn)顟B(tài)機(jī)概要文件可以包含狀態(tài)(State)、遷移條件(Transition)、區(qū)域(Region)、活動(dòng)(Activity)等元素的擴(kuò)展，具體的擴(kuò)展元素根據(jù)實(shí)際需要進(jìn)行選取。本文主要對(duì)混成自動(dòng)機(jī)的狀態(tài)(State)、狀態(tài)內(nèi)部包含的流條件(FlowCondition)、不等式條件(InvariantCondition) 和遷移條件(Transition)進(jìn)行了擴(kuò)展。其中，ModeState對(duì)元類State進(jìn)行了擴(kuò)展。見圖2，擴(kuò)展?fàn)顟B(tài)概要文件描述了擴(kuò)展?fàn)顟B(tài)(ModeState)與表達(dá)式(Expression)和約束(Constraint)之間的關(guān)系。其中，Stereotype 表示構(gòu)造型，metaclass表示UML已經(jīng)定義的元類元素。構(gòu)造型ModeState具有Constraint和Expression兩種屬性。Expression(約束)有InvExpression(狀態(tài)變量滿足的不等式約束)和stateFlow(狀態(tài)變量微分滿足的約束)兩種形式。 iniState{subsets ownedRule}表示初始狀態(tài)(iniState)具有的屬性。

1.2 由HUML模型到HYTECH模型的轉(zhuǎn)換規(guī)則

根據(jù)HYTECH模型的結(jié)構(gòu)定義[10]，將擴(kuò)展后建立的HUML模型轉(zhuǎn)化為HYTECH形式化模型，主要有以下方面：

(1) 系統(tǒng)組成

HYTECH模型由個(gè)或多個(gè)自動(dòng)機(jī)模塊(Automaton)和系統(tǒng)分析操作指令兩部分組成。自動(dòng)機(jī)模塊描述系統(tǒng)所有包含的離散狀態(tài)(Location)，各離散狀態(tài)之間的遷移過(guò)程，以及離散狀態(tài)內(nèi)部的連續(xù)變化過(guò)程。HYTECH模型中系統(tǒng)分析操作命令部分包括region變量的聲明(包括initial region和final region)、系統(tǒng)的組成結(jié)構(gòu)及根據(jù)模型分析的類型聲明不同的分析操作指令。在進(jìn)行安全分析時(shí)，final region一般為危險(xiǎn)狀態(tài)集，initial region為系統(tǒng)的初始狀態(tài)集。根據(jù)不同的分析目的編寫分析操作指令模塊部分。

(2) 自動(dòng)機(jī)模塊

HYTECH模型中的自動(dòng)機(jī)模塊對(duì)應(yīng)HUML的擴(kuò)展類(《Agent》)和擴(kuò)展?fàn)顟B(tài)機(jī)中的狀態(tài)(《Mode State》)，包含系統(tǒng)的靜態(tài)屬性及動(dòng)態(tài)行為描述。每個(gè)自動(dòng)機(jī)包含有一個(gè)或者多個(gè)狀態(tài)(loc)，以及所有離散狀態(tài)之間的遷移(Transition)。每個(gè)location包含有對(duì)應(yīng)離散狀態(tài)的invariant condition和flow condition描述。完整的自動(dòng)機(jī)模塊由變量聲明(var)、標(biāo)簽定義(synclabs)、狀態(tài)描述(loc)以及遷移過(guò)程(transition)的定義等幾部分組成。

(3) 系統(tǒng)變量聲明

離散狀態(tài)(loc)的連續(xù)變量類型有模擬型(analog)，時(shí)鐘型(clock)，計(jì)時(shí)類型(stopwatch)等，其中clock的變化率為1，stopwatch的變化率或?yàn)?或?yàn)?，analog類型變量的變化率沒有限制。離散控制變量對(duì)應(yīng)discrete類型變量，其變化率為0。待確定的參數(shù)值為parameter類型的變量，其變化率為0且不能進(jìn)行賦值，以及常量(由define 語(yǔ)句進(jìn)行定義)的聲明。

(4) 標(biāo)簽定義

標(biāo)簽定義以關(guān)鍵字synclabs作為標(biāo)記。該標(biāo)簽的定義主要是用于同步各自動(dòng)機(jī)的共享事件，尤其在并發(fā)分布式系統(tǒng)中具有重要的作用。對(duì)應(yīng)于HUML模型中的遷移觸發(fā)事件。

(5) 狀態(tài)描述

在離散狀態(tài)loc中，flow condition對(duì)應(yīng)于wait關(guān)鍵詞所標(biāo)記的內(nèi)容，用于描述狀態(tài)loc所包含變量的變化率，一般是由區(qū)間或常量表示。invariant condition對(duì)應(yīng)于while關(guān)鍵詞標(biāo)記的內(nèi)容，描述狀態(tài)所含變量須滿足的不等式約束集。

(6) 遷移過(guò)程的定義

遷移過(guò)程的具體定義以關(guān)鍵字when開始。每1遷移對(duì)應(yīng)于1條when…do…goto語(yǔ)句。loc關(guān)鍵詞標(biāo)記對(duì)應(yīng)遷移的源狀態(tài)(source location)，when關(guān)鍵詞后是對(duì)應(yīng)遷移的遷移衛(wèi)式(guard)，do關(guān)鍵詞后是對(duì)應(yīng)遷移的置位表達(dá)式(reset)，goto關(guān)鍵詞后是對(duì)應(yīng)遷移的目標(biāo)狀態(tài)(target location)。當(dāng)守衛(wèi)條件無(wú)約束時(shí)，guard為True。發(fā)生遷移后變量的值保持不變，則reset可以表示為v′=v(v′表示變量v的下一狀態(tài)，v表示變量v的當(dāng)前狀態(tài))。發(fā)生遷移后，變量的值不確定表示為x′=x。

(7)系統(tǒng)分析操作指令模塊

分析操作指令部分包括region變量的聲明(包括initial region和final region)，系統(tǒng)的組成結(jié)構(gòu)，以及根據(jù)模型分析的不同目的聲明不同的分析操作指令。在進(jìn)行安全分析時(shí)，final region一般為危險(xiǎn)狀態(tài)集，用于描述系統(tǒng)最終所處的狀態(tài)，對(duì)應(yīng)于系統(tǒng)的安全性需求的形式化描述。initial region定義了組成系統(tǒng)的自動(dòng)機(jī)組合和各自動(dòng)機(jī)中的變量所滿足的初始狀態(tài)集，對(duì)應(yīng)于HUML所包含的擴(kuò)展類Agent和各自動(dòng)機(jī)的初始狀態(tài)集(Initial Constraint)。

1.3 混成自動(dòng)機(jī)模型中未知控制參數(shù)的分析

HYTECH模型通過(guò)計(jì)算系統(tǒng)的可達(dá)集分析系統(tǒng)模型的未知參數(shù)?？蛇_(dá)集的計(jì)算有前向可達(dá)集計(jì)算和后向可達(dá)集計(jì)算兩種?！畆each forward from 〈reg_exp〉 endreach’用于表示前向可達(dá)集計(jì)算的操作指令，其中reg_exp表示系統(tǒng)的初始狀態(tài)集合。當(dāng)final_region與可達(dá)集的交集為空時(shí)，表示滿足系統(tǒng)的安全性需求。否則，模型不滿足安全性需求。‘reach backward from〈reg_exp〉 endreach’表示后向可達(dá)集計(jì)算指令，其中reg_exp一般為final_reg，在安全分析中，final_reg一般表示危險(xiǎn)狀態(tài)集合。通過(guò)不斷向前迭代的方式，當(dāng)final_reg的可達(dá)集與initial_reg的交集為空時(shí)，表示滿足系統(tǒng)的安全性需求。否則，不滿足安全性需求。

2 案例分析

2.1 場(chǎng)景描述

傳統(tǒng)的信號(hào)控制系統(tǒng)是基于固定閉塞的控制系統(tǒng)，未考慮列車的不同速度和制動(dòng)性能，閉塞區(qū)間的長(zhǎng)度固定不變，這影響軌道的利用效率。移動(dòng)閉塞取消了固定的閉塞區(qū)間劃分，閉塞區(qū)間間隔隨列車的運(yùn)行動(dòng)態(tài)變化，降低了列車運(yùn)行間隔時(shí)間，提高了軌道的利用效率。移動(dòng)閉塞追蹤模型見圖3，圖3中包含的要素有列車定位(Train Position)、安全距離(Safety Distance)和目標(biāo)點(diǎn)(Target Point)。其中，安全距離是列車實(shí)施最大常用制動(dòng)的附加距離，保證列車在最壞的情況下列車不發(fā)生追尾，用圖3中的SD表示。目標(biāo)點(diǎn)是列車當(dāng)前時(shí)刻能夠運(yùn)行到的最遠(yuǎn)點(diǎn)，相當(dāng)于列車的移動(dòng)授權(quán)。

在圖3中橫坐標(biāo)表示列車運(yùn)行的位置，縱坐標(biāo)表

示后行列車在各位置點(diǎn)所對(duì)應(yīng)的速度，SBI表示最大常用制動(dòng)曲線，EBI表示緊急制動(dòng)曲線，SD表示安全距離，EOA_SB和EOA_EB分別表示常用制動(dòng)曲線和緊急制動(dòng)曲線的終點(diǎn)，REL表示列車的緩解速度曲線，SBD表示列車開始實(shí)施制動(dòng)時(shí)的位置點(diǎn)。

2.2 建立移動(dòng)閉塞追蹤模型的線性混成自動(dòng)機(jī)模型

在實(shí)際的運(yùn)營(yíng)過(guò)程中，某區(qū)段中有多輛列車同時(shí)運(yùn)行，為簡(jiǎn)便起見，該模型僅考慮兩輛列車單向追蹤的場(chǎng)景。根據(jù)移動(dòng)閉塞系統(tǒng)工作原理，建立后行列車的距離控制器的線性混成自動(dòng)機(jī)模型，見圖4。由于該模型中包含有未知控制參數(shù)，因此屬于抽象混成自動(dòng)機(jī)模型。并假定前行列車為勻速行駛，后行列車實(shí)施制動(dòng)(緊急制動(dòng)或常用制動(dòng))時(shí)的加速度為恒定值，即不考慮列車加速和實(shí)施制動(dòng)時(shí)達(dá)到最大加速度和最大制動(dòng)能力所需的延遲時(shí)間。在該模型中，不考慮列車的制動(dòng)距離，僅考慮兩列車之間的安全防護(hù)距離，取為400 m。相鄰列車的追蹤間隔由距離控制器控制，確保兩車的間隔不小于400 m，從而保證兩車不發(fā)生追尾事故。該控制器連續(xù)不斷與無(wú)線閉塞中心RBC保持通信，接收列車的位置和速度信息，并通過(guò)計(jì)算得到兩車間的距離。后行列車最大速度vmax為220 km/h，最小速度為0。運(yùn)用Δ表示從RBC接收到的2個(gè)MA信息的時(shí)間間隔，因此，不再考慮移動(dòng)閉塞系統(tǒng)中不同模塊間的交互過(guò)程。

距離控制器模型包含有7個(gè)狀態(tài)：idle(靜止), acc(加速), max_speed(最大速度運(yùn)行), eb(緊急制動(dòng)), sb(常用制動(dòng)), release(緩解制動(dòng))和crash(危險(xiǎn)狀態(tài))。模型中，x表示兩相鄰列車之間的距離間隔。xf,vf和af分別表示后行列車的前端位置，速度和加速度值。xl,vl和al分別表示前行列車的尾部位置，速度和加速度值(本文中位置、速度和加速度的單位分別為m、km/h和m/s2，以下同)。參數(shù)D_eb，D_sb，D_rele和D_acc表示該控制模型的控制參數(shù)，當(dāng)列車間隔達(dá)到對(duì)應(yīng)的值時(shí)，將會(huì)觸發(fā)狀態(tài)相應(yīng)的遷移。在遷移過(guò)程中，位置(xf、xl)和速度(vf、vl)的值不能被重置，根據(jù)所進(jìn)入的狀態(tài)，加速度af的值可以被重置。

模型中各狀態(tài)對(duì)應(yīng)的不等式約束和流條件為：除crash(危險(xiǎn)狀態(tài))之外，其他所有所有狀態(tài)都滿足的不等式約束為：‘(x=xl-xf)∧(xf≥0)∧(xl≥0)∧(vl=140)∧(al=0)∧(Δ=3)’。所有狀態(tài)滿足的流條件為：‘(dx=dxl-dxf)∧(dxf=39)∧(dvl=0)∧(dal=0)’，其中dx,dv,da分別表示列車的位置、速度和加速度的變化率。

圖4中各狀態(tài)所對(duì)應(yīng)的不等式條件Inv和對(duì)應(yīng)的流條件Flow分別為

( 1 )

( 2 )

模型的遷移條件有遷移衛(wèi)式和置位條件兩種表達(dá)式。例如，x=D_eb表示的是遷移衛(wèi)式，a:=-25為置位條件表達(dá)式。

列車的運(yùn)動(dòng)過(guò)程簡(jiǎn)述如下：初始時(shí)刻，后行列車可能處于靜止或以最大速度運(yùn)行。當(dāng)列車之間的間隔大于零且小于D_eb時(shí)，列車實(shí)施緊急制動(dòng)；當(dāng)間隔大于D_eb且小于D_sb時(shí)，列車實(shí)施常用制動(dòng)；當(dāng)間隔小于0時(shí)，列車進(jìn)入crash(危險(xiǎn)狀態(tài))。緊急制動(dòng)只有在列車停車后才能緩解，在兩車的間隔大于D_rele時(shí)，可以緩解常用制動(dòng)。當(dāng)列車間的間隔大于D_acc時(shí)，后行列車將進(jìn)入加速狀態(tài)。所有控制參數(shù)的取值或取值范圍不僅取決于列車的加速和制動(dòng)性能，而且還與系統(tǒng)規(guī)定的安全性需求有關(guān)。

2.3 模型的轉(zhuǎn)換及參數(shù)分析過(guò)程2.3.1 轉(zhuǎn)換后的HYTECH模型片段

根據(jù)上述提出的轉(zhuǎn)換規(guī)則，將HUML模型轉(zhuǎn)換為可執(zhí)行的HYTECH模型，控制器的HYTECH模型片段見表1。為了保證模型本身的正確性，首先需要驗(yàn)證模型的可達(dá)性，即當(dāng)初始域(系統(tǒng)的初始狀態(tài)滿足的約束集)包括所有可能的初始狀態(tài)時(shí)，控制器的所有狀態(tài)(除危險(xiǎn)狀態(tài)外)必須為可達(dá)。若存在不可達(dá)狀態(tài)，則表明該模型不完整需要修改模型。其次，根據(jù)系統(tǒng)的安全性需求，計(jì)算未知控制參數(shù)的約束集。為了說(shuō)明所提出方法的有效性，以下首先對(duì)模型的可達(dá)集進(jìn)行計(jì)算，然后給出控制參數(shù)約束集的生成過(guò)程。

表1 HYTECH模型片段

2.3.2 驗(yàn)證抽象HYTECH模型狀態(tài)的可達(dá)性

根據(jù)提出的轉(zhuǎn)換規(guī)則，將HUML模型轉(zhuǎn)換為HYTECH模型，驗(yàn)證HYTECH模型的可達(dá)性。當(dāng)追蹤列車初始時(shí)刻處于idle狀態(tài)且列車之間的距離區(qū)間為[800 m，3 000 m](即初始域：initial_region={loc[sys]=idle&x>800 &x≤3 000})，追蹤列車的加速和制動(dòng)性能見圖4距離控制器模型所示，系統(tǒng)所含控制參數(shù)須滿足的約束可根據(jù)實(shí)際情況決定。為方便分析規(guī)定未知參數(shù)所滿足的約束不等式為‘(200≤D_eb≤D_sb≤D_rele≤D_acc)’。

對(duì)于該初始域及參數(shù)約束，計(jì)算得到可達(dá)狀態(tài)集為StateSet={idle,acc,max_speed, sb,eb,release}，可達(dá)狀態(tài)對(duì)應(yīng)的可達(dá)集如下：

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}；

為簡(jiǎn)潔起見，以上所列出的約束表達(dá)式中略去該狀態(tài)初始定義時(shí)所滿足的約束表達(dá)式，僅列出滿足安全需求性指標(biāo)時(shí)的可達(dá)集約束。當(dāng)模型的可達(dá)集中包含有不允許出現(xiàn)的狀態(tài)(列車追尾、超速或其他危險(xiǎn)狀態(tài))時(shí)，需要對(duì)模型的控制參數(shù)進(jìn)行修正，直到可達(dá)狀態(tài)集中不包含危險(xiǎn)狀態(tài)為止。只有在保證模型滿足可達(dá)性的前提下才能對(duì)參數(shù)進(jìn)行分析。由StateSet結(jié)果可見，該模型可達(dá)集中不包含crash狀態(tài)且其他狀態(tài)都可達(dá)，因此該模型滿足可達(dá)性的基本屬性，可以進(jìn)行下一步的分析。

2.3.3 控制參數(shù)約束集的計(jì)算

在保證可達(dá)性屬性后，計(jì)算滿足安全性需求的控制參數(shù)約束集。初始域(Initial_reg)表示系統(tǒng)對(duì)應(yīng)的初始狀態(tài)及狀態(tài)約束集。目標(biāo)集(Final_reg)表示控制器的禁止?fàn)顟B(tài)，其中‘loc[sys]=crash’表示相鄰的列車發(fā)生碰撞，‘x≤400’表示列車間隔低于400 m，‘x≥7 000’表示列車間隔大于7 000 m。其中，‘x≤400’是為了保證安全需求，而‘x≥7 000’是為了保證軌道的利用效率。控制參數(shù)約束集(ConstraintSet)的意義是：當(dāng)系統(tǒng)初始狀態(tài)滿足初始域時(shí)，為了使系統(tǒng)不處于目標(biāo)集狀態(tài)，所有的控制參數(shù)必須滿足的不等式約束。也即控制參數(shù)滿足約束集ConstraintSet時(shí)，不僅可以保證系統(tǒng)為安全，同時(shí)能夠提高軌道的利用效率。追蹤列車的加速和制動(dòng)性能如模型中所示。目標(biāo)集定義為：列車之間的距離大于400 m小于7 000 m且兩車不發(fā)生追尾，即Final_region={x≥7 000∨x≤400&vf>0∨loc[sys]=crash}。下面分析不同的初始狀態(tài)和安全性指標(biāo)，控制參數(shù)須滿足的約束集，其中IRi表示系統(tǒng)的初始狀態(tài)，CSi表示對(duì)應(yīng)參數(shù)的約束集合。

(1) 初始時(shí)列車處于idle狀態(tài)，與前行列車距離區(qū)間為[800，3 000]，運(yùn)行速度為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) 初始時(shí)列車處于max_speed狀態(tài)且與前行列車距離區(qū)間為[800，3 000]，運(yùn)行速度為220 km/h。

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

(3) 初始時(shí)列車處于acc狀態(tài)，與前行列車距離區(qū)間為[3 000，6 000]，運(yùn)行速度為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) 初始時(shí)列車處于idle狀態(tài)，與前行列車距離區(qū)間為[3 000，6 000]，運(yùn)行速度為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) 初始時(shí)列車處于acc狀態(tài)，運(yùn)行速度為200 km/h，與前行列車距離區(qū)間為[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)}

對(duì)于具有不同性能的列車滿足相同安全需求(Final_reg={loc[sys]=crash∨x≥7 000∨x≤400})的情況，可以根據(jù)列車性能計(jì)算得到不同的控制參數(shù)約束集，從而實(shí)現(xiàn)控制模型的重用。Initial_reg和Final_reg分別表示初始域和目標(biāo)域，ParaConsSet表示控制參數(shù)約束集。下面分別對(duì)3種性能的列車進(jìn)行分析，分析結(jié)果為:

(1) 列車的加速度為4 m/s2，常用制動(dòng)減速度為-8 m/s2，緊急制動(dòng)減速度為-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，常用制動(dòng)減速度為-10 m/s2，緊急制動(dòng)減速度-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，常用制動(dòng)減速度為-8 m/s2，緊急制動(dòng)減速度為-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 控制參數(shù)約束集驗(yàn)證

為證明所得控制參數(shù)約束的正確性，以下對(duì)約束集進(jìn)行驗(yàn)證。當(dāng)指定模型的控制參數(shù)值時(shí)，可以計(jì)算兩車距離的區(qū)間范圍。由上述分析結(jié)果知，系統(tǒng)初始域定義為

Initial_reg=(Loc[sys]=idle)&(xl>xf)&(x≥800)&(x≤3 000)&(vf=0)&(af=0)時(shí)，由安全需求定義系統(tǒng)的目標(biāo)集為Final_reg=loc[sys]=crash∨x≥7 000∨x≤400，計(jì)算得到參數(shù)約束集為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。因此，控制參數(shù)取為：D_eb=400,D_sb=500,D_rele=700,D_acc=850”，根據(jù)這組控制參數(shù)計(jì)算列車間隔的區(qū)間。用distancemin和distancemax分別表示距離的最小值和最大值，它們都表示恒定不變的符號(hào)常量，將其引入到Final_reg，F(xiàn)inal_reg={loc[sys]=crash∨x≤distancemin∨x≥distancemax}，然后進(jìn)行可達(dá)性分析。當(dāng)狀態(tài)acc，eb，sb處的加速度值分別為4、-15、-8 m/s2時(shí)，對(duì)應(yīng)的輸出結(jié)果為distancemax≥2 295,distancemin>500 m。由該結(jié)果知，兩列車的最大距離間隔為2 295 m，最小距離間隔為500 m。因而，當(dāng)控制參數(shù)滿足‘(D_sb≥400∨D_acc≤800)&(D_acc≤800∨D_eb≥400∨D_acc>884)&(D_eb≤800)’時(shí)，追蹤列車之間的距離區(qū)間為[500,2 295]，該區(qū)間包含于[400,7 000]，即所選控制參數(shù)滿足對(duì)應(yīng)的安全性需求。

3 結(jié)束語(yǔ)

本文針對(duì)混成系統(tǒng)模型，在滿足安全性需求的前提下，為推導(dǎo)線性混成自動(dòng)機(jī)模型中未知控制參數(shù)之間所須滿足的約束不等式，提出了未知參數(shù)分析方法。運(yùn)用該方法可求解與安全性需求對(duì)應(yīng)的參數(shù)約束集，從而保證控制系統(tǒng)的安全運(yùn)行。最后以移動(dòng)閉塞中的追蹤模型為例，建立追蹤模型控制器對(duì)應(yīng)的HUML模型，運(yùn)用所提出的方法對(duì)其進(jìn)行分析，得到距離控制參數(shù)的約束集，并對(duì)所得到的參數(shù)結(jié)果進(jìn)行驗(yàn)證。驗(yàn)證結(jié)果表明，得到的參數(shù)約束集能夠滿足系統(tǒng)的安全性需求。對(duì)于在線路上運(yùn)行的性能不同的列車，可根據(jù)列車的性能參數(shù)生成不同的控制參數(shù)模型，實(shí)現(xiàn)控制模型的復(fù)用。

參考文獻(xiàn)：

[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ìn)程的高速鐵路列控系統(tǒng)形式化建模與驗(yàn)證方法[J].中國(guó)鐵道科學(xué),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.