宋 莉，劉伯鴻

（蘭州交通大學(xué) 自動化與電氣工程學(xué)院，蘭州730070）

臨時限速是列車控制系統(tǒng)的核心構(gòu)成之一，是一種安全苛求系統(tǒng)[1]。臨時限速命令的操作過程主要基于人們長期經(jīng)驗和直覺積累的技術(shù)規(guī)范，而這些技術(shù)規(guī)范一般以自然語言定義，或多或少地存在二義性和不確定性。技術(shù)規(guī)范的任一缺陷若處理不當(dāng)，將會演變成系統(tǒng)故障。

作為典型的實時系統(tǒng)，臨時限速涉及多個設(shè)備之間的復(fù)雜交互。形式化方法不僅用于描述實值時鐘約束系統(tǒng)，也可用于描述具有有限控制變量的狀態(tài)切換系統(tǒng)[2]。時間自動機基于自動機理論，增加了時間因素，可以描述臨時限速系統(tǒng)的連續(xù)時間特性和復(fù)雜的信息交互特性，在列控領(lǐng)域已有相關(guān)的研究案例[3-5]。為臨時限速系統(tǒng)建立時間自動機模型，可以有效地識別時間受限的缺陷，對其安全性和受限活性進行分析，對于驗證臨時限速技術(shù)規(guī)范的正確性具有重要意義。

1 臨時限速系統(tǒng)構(gòu)成

作為一種安全苛求系統(tǒng)，臨時限速系統(tǒng)負(fù)責(zé)與其它列車控制系統(tǒng)的信息交互，對列車的安全運行和效率起著至關(guān)重要的作用[6]。圖1描述了臨時限速系統(tǒng)的系統(tǒng)結(jié)構(gòu)及命令傳輸通道。

調(diào)度集中系統(tǒng)（CTC，Centralized TrafficControl）調(diào)度中心負(fù)責(zé)下達(dá)擬定、執(zhí)行、取消限速命令；臨時限速服務(wù)器（TSRS，TemporarySpeedRestriction Server）負(fù)責(zé)存儲、驗證、分發(fā)臨時限速命令（TSR，TemporarySpeedRestriction）[7]；列控中心（TCC，TrainControlCenter）與無線閉塞中心（RBC，RadioBlockCenter）主要負(fù)責(zé)檢查臨時限速命令的有效性，生成臨時限速信息包（無線消息和CTCS報文），并分別通過應(yīng)答器、無線GSM-R 將TSR 命令發(fā)送到車載設(shè)備執(zhí)行。2臨時限速系統(tǒng)建模分析

圖1 臨時限速系統(tǒng)構(gòu)成示意

2.1 時間自動機理論

時間自動機理論在傳統(tǒng)的自動機基礎(chǔ)上增加了時鐘約束機制，并引入有窮圖注釋狀態(tài)轉(zhuǎn)換，可以更好地表達(dá)實時系統(tǒng)的時間約束特性[8]。

時間自動機TA是一個六元組，TA=，其中：S為一組位置，S0為一組初始位置，A為一組觸發(fā)事件通道，X為一組時間參數(shù)，I是一組映射位置，將每個位置變量參數(shù)S指定Φ（x）中的時間約束為狀態(tài)轉(zhuǎn)換[9]。

2.2 臨時限速系統(tǒng)時間自動機網(wǎng)絡(luò)

臨時限速系統(tǒng)中的信息交互主要涉及4 個系統(tǒng)，即TCC、TSRS、CTC和RBC。由于TCC與RBC臨時限速命令信息的類型相似，為簡化模型，僅選擇CTC、TSRS和RBC（TCC）作為建模對象[10]。

臨時限速系統(tǒng)的每一次信息交互都需要CTC子系統(tǒng)、TSRS子系統(tǒng)、RBC（TCC）子系統(tǒng)同步工作、協(xié)同完成，每個子系統(tǒng)模型均稱為時間自動機，子系統(tǒng)之間的通信交互稱為每個時間自動機之間的通信交互，即有TA=TACTC||TATSRS||TARBC（TCC）。

2.3 BNF語法

UPPAAL 的驗證器為模型的性質(zhì)驗證提供一種規(guī)范的驗證語言—BNF（BackusNaurForm）自動機語言，其定義如下：

其中，各語句的含義見表1。

表1 BNF語句及其含義

2.4 臨時限速系統(tǒng)實時性要求

臨時限速工作流程由臨時限速的擬定、執(zhí)行和取消3部分組成[11]。實時性要求主要包括安全性和受限活性；安全性是指系統(tǒng)中未必會發(fā)生的事情，而受限活性是指系統(tǒng)中必定會發(fā)生的事情。

2.4.1 安全性要求

（1）系統(tǒng)能夠設(shè)置、驗證、執(zhí)行、取消臨時限速命令[12]；

（2）CTC可以完成臨時速度限制命令的擬定、設(shè)置、取消；

（3）CTC激活命令失敗可重新激活或撤銷激活；

（4）系統(tǒng)能夠檢測各個設(shè)備限速命令的一致性和有效性；

（5）TSRS對限速命令先驗證再執(zhí)行；

（6）TSRS分發(fā)執(zhí)行、取消等操作命令到RBC（TCC），且RBC（TCC）將執(zhí)行結(jié)果反饋給TSRS。

2.4.2 受限活性要求

（1）系統(tǒng)不存在死鎖現(xiàn)象；

（2）在收到TSR 指令后，RBC能夠在TRBCreaction時間內(nèi)返回ExecuteResult 指令；

（3）如果在TTSRStimeout時間內(nèi)沒有將反饋信息發(fā)送到TSRS，則重發(fā)；如果超過TTSRStimeout時間，則發(fā)出Warning指令報警。

3 臨時限速工作流程模型

基于臨時限速工作流，使用UPPAAL 工具建立時間自動機模型。在模型中，a!表示發(fā)出一個事件a，a?表示相應(yīng)地同步接收一個事件a。緊迫位置標(biāo)有符號U，表示沒有時間延遲，減少分析的復(fù)雜度；堅定位置用C標(biāo)注，表示下一次過渡必須毫不拖延地離開一個或多個堅定位置[13]。

3.1 CTC臨時限速模型

CTC負(fù)責(zé)下達(dá)擬定、執(zhí)行、取消限速命令。根據(jù)時間自動機理論，建立CTC自動機模型，如圖2所示。

圖2 CTC臨時限速模型

用SC T C描述圖中各功能位置，SC T C={i d l e,S_CheckFailure,S_CheckSucess,S_ActivateTSR,S_ActivateSucess,S_ManualHandle,S_VerfSuccess,S_PromptSet,S_ConfirmSet,exeTSR,S_ExeFailure,F_SendTSR,S_ExeSuccess,F_PreTSR},初始狀態(tài)idle,觸發(fā)事件：checkSuccess,checkFailure,TSRFailure,Revocation,reActive,activate,VerfSuccess,VerfFailure,warning,plannedTSR,confExecute,F_reset,TSRFailure,TSRSuccess,exeSuccess12,F_cancelTSR。

結(jié)合信息交互流程，TACTC的主要位置見表2。

表2 TACTC的主要位置

3.2 TSRS臨時限速模型

TSRS負(fù)責(zé)存儲、驗證、分發(fā)TSR 命令，是臨時限速系統(tǒng)的核心。利用時間自動機理論，建立TSRS自動機模型，如圖3所示。

用STSRS描述圖中各功能位置，STSRS={idle,S_NoticeRBC,S_StoreList,S_TSRsuccess,S_JudExeResult,S_RecExeResult,S_WaitResult,S_TSRFail,S_PreExe,S_WaitConfirm,S_JudgeResult,S_RecResult,S_WaitCheck,S_DistinguishRBC,S_Active,S_VerfFail,S_WaitActive,F_FeedBackFailure,F_CheckFailure,F_RecTSR,F_CheckVaildity,F_CheckSuccess,F_PromptActivate},初始狀態(tài)idle,觸發(fā)事件：checkSuccess,checkFailure,TSRFailure,

圖3 TSRS臨時限速模型

Revocation,reActive,activate,VerfSuccess,VerfFailure1,warning,plannedTSR1,confExecute,F_reset,TSRFailure,TSRSuccess,exeSuccess12,F_cancelTSR,ExecuteResult,ExecuteTSR,CheckResult,TSR1。

結(jié)合信息交互流程，TATSRS的主要位置見表3。

表3 TATSRS的主要位置

3.3 RBC（TCC）臨時限速模型

RBC與TCC主要負(fù)責(zé)檢查臨時限速命令的有效性，生成臨時限速信息包（無線消息和CTCS報文），并分別通過無線GSM-R、應(yīng)答器將TSR 發(fā)送到車載設(shè)備執(zhí)行。根據(jù)時間自動機理論，建立RBC（TCC）自動機模型，如圖4 所示。

圖4 RBC（TCC）臨時限速模型

用SRBC(TCC)描述圖中各功能位置，SRBC(TCC)={idle,S_SendtoTrain,S_ExeSuccess,S_CheckValidity,S_SendResult,S_ExeTSR,S_ExeFinsh}，初始狀態(tài)idle，觸發(fā)事件：TSR1，reAvtive，CheckResult，F(xiàn)_cancelTSR，ExecuteTSR，exeSuccess12，F(xiàn)_reset，ExecuteResult。

結(jié)合信息交互流程，TARBC（TCC）的主要位置見表4。

表4 TARBC(TCC)的主要位置

4 模型仿真與驗證

在驗證系統(tǒng)的性質(zhì)之前，需要解決“所建立的模型是否是一個與實際系統(tǒng)一致的、正確的數(shù)學(xué)模型”的問題。從兩個方面解決此問題：

（1）從規(guī)范中提出有意義的驗證目標(biāo)；

（2）根據(jù)臨時限速系統(tǒng)技術(shù)規(guī)范，正確使用BNF 驗證語句[14]。

4.1 模型仿真

使用UPPAAL 工具中Simulator 模塊仿真驗證臨時限速系統(tǒng)模型，以檢查模型中是否存在語法錯誤。仿真過程與臨時限速工作流程相平行，以保證模型的完整性與一致性，可視化描述信息交互路徑，仿真過程如圖5所示。

4.2 結(jié)果驗證

通過時間自動機的可訪問性分析驗證其安全性、位置不變性和傳輸約束，保證系統(tǒng)的受限活性[15]。以“CTC可以完成臨時速度限制命令的擬定、設(shè)置、取消”為例，此安全功能屬性的BNF 驗證語句可寫為：E[]((CTC.idle)imply(CTC.S_Check Success)and

(TSRS.F_Check Success)imply(TSRS.S_Wait Active))。

其中，(CTC.idle)imply(CTC.S_Check Success)表示時間自動機TACTC可以從狀態(tài)(idle，v)到達(dá)狀態(tài)(S_Check Success，v)，即CTC發(fā)出擬定、執(zhí)行和取消臨時限速命令plannedTSR1。(TSRS.F_Check Success)imply(TSRS.S_Wait Active)表示時間自動機TATSRS可以從狀態(tài)(F_Check Success，v)到達(dá)狀態(tài)(S_Wait Active，v)，即TSRS收到CTC發(fā)出的臨時限速命令，并反饋Check Success命令。

如果UPPAAL 驗證式?jīng)]有通過，表示系統(tǒng)中任何執(zhí)行序列中的任何狀態(tài)都不滿足表達(dá)式(CTC.idle)imply(CTC.S_Check Success)and(TSRS.F_Check Success)imply(TSRS.S_Wait Active)，系統(tǒng)的安全性由此得以驗證。圖6為臨時限速系統(tǒng)模型驗證截圖。

圖6 臨時限速系統(tǒng)模型驗證截圖

在UPPAAL 的Verify屬性列表中，逐個輸入要驗證的BNF 描述語句。表5列出臨時限速系統(tǒng)需驗證的性質(zhì)及對應(yīng)的BNF 驗證語言，對表中性質(zhì)進行驗證，得出每條性質(zhì)都是安全的。

5 結(jié)束語

臨時限速系統(tǒng)的實時性要求極高?；谂R時限速的工作流程，結(jié)合時間自動機理論和UPPAAL 工具，對臨時限速系統(tǒng)進行建模仿真及驗證。結(jié)果表明：臨時限速系統(tǒng)的安全性和受限活性均滿足要求，驗證了系統(tǒng)的實時性。

臨時限速系統(tǒng)的建模和驗證，為系統(tǒng)的設(shè)計和開發(fā)提供了依據(jù)，對系統(tǒng)的進一步測試和故障分析起著重要作用。

表5 臨時限速系統(tǒng)需滿足的性質(zhì)