基于UPPAAL的列控系統(tǒng)臨時(shí)限速建模與驗(yàn)證

宋 莉，劉伯鴻

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

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

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

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

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

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

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

2.1 時(shí)間自動機(jī)理論

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

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

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

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

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

2.3 BNF語法

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

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

表1 BNF語句及其含義

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

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

2.4.1 安全性要求

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

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

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

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

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

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

2.4.2 受限活性要求

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

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

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

3 臨時(shí)限速工作流程模型

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

3.1 CTC臨時(shí)限速模型

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

圖2 CTC臨時(shí)限速模型

用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臨時(shí)限速模型

TSRS負(fù)責(zé)存儲、驗(yàn)證、分發(fā)TSR 命令，是臨時(shí)限速系統(tǒng)的核心。利用時(shí)間自動機(jī)理論，建立TSRS自動機(jī)模型，如圖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臨時(shí)限速模型

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）臨時(shí)限速模型

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

圖4 RBC（TCC）臨時(shí)限速模型

用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 模型仿真與驗(yàn)證

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

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

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

4.1 模型仿真

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

4.2 結(jié)果驗(yàn)證

通過時(shí)間自動機(jī)的可訪問性分析驗(yàn)證其安全性、位置不變性和傳輸約束，保證系統(tǒng)的受限活性[15]。以“CTC可以完成臨時(shí)速度限制命令的擬定、設(shè)置、取消”為例，此安全功能屬性的BNF 驗(yàn)證語句可寫為：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)表示時(shí)間自動機(jī)TACTC可以從狀態(tài)(idle，v)到達(dá)狀態(tài)(S_Check Success，v)，即CTC發(fā)出擬定、執(zhí)行和取消臨時(shí)限速命令plannedTSR1。(TSRS.F_Check Success)imply(TSRS.S_Wait Active)表示時(shí)間自動機(jī)TATSRS可以從狀態(tài)(F_Check Success，v)到達(dá)狀態(tài)(S_Wait Active，v)，即TSRS收到CTC發(fā)出的臨時(shí)限速命令，并反饋Check Success命令。

如果UPPAAL 驗(yàn)證式?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)的安全性由此得以驗(yàn)證。圖6為臨時(shí)限速系統(tǒng)模型驗(yàn)證截圖。

圖6 臨時(shí)限速系統(tǒng)模型驗(yàn)證截圖

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

5 結(jié)束語

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

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

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