趙榮亮，王長(zhǎng)林

(西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610031)

臨時(shí)限速系統(tǒng)是高速鐵路列車控制（簡(jiǎn)稱：列控）系統(tǒng)的重要組成部分，臨時(shí)限速的設(shè)置直接關(guān)系到列車的運(yùn)行效率和運(yùn)行安全。臨時(shí)限速分為突發(fā)限速和有計(jì)劃情況下的限速，僅在某段線路上一定的時(shí)間范圍內(nèi)有效，其工作流程即擬定、設(shè)置、執(zhí)行、取消等具有嚴(yán)格的時(shí)間約束特性，是典型的實(shí)時(shí)系統(tǒng)。根據(jù)列車的實(shí)際運(yùn)行情況，臨時(shí)限速區(qū)段可能設(shè)置在調(diào)度集中系統(tǒng)調(diào)度臺(tái)分界處，此時(shí)，臨時(shí)限速系統(tǒng)與相鄰的調(diào)度臺(tái)之間都有信息交互，表現(xiàn)出的交互特性更加復(fù)雜。

形式化方法以數(shù)學(xué)為基礎(chǔ)，運(yùn)用嚴(yán)格的方法和語(yǔ)義對(duì)系統(tǒng)特性或行為進(jìn)行精確描述[1]，根據(jù)描述模型，可以最大限度地驗(yàn)證系統(tǒng)的正確性。時(shí)間自動(dòng)機(jī)是對(duì)自動(dòng)機(jī)理論的擴(kuò)展，不僅可用來(lái)描述系統(tǒng)的時(shí)間特性，還能很好的描述系統(tǒng)的交互特性?；跁r(shí)間自動(dòng)機(jī)理論的驗(yàn)證工具UPPAAL為用戶提供了良好的建模仿真界面，并且能夠自動(dòng)對(duì)系統(tǒng)的屬性進(jìn)行驗(yàn)證。

本文基于時(shí)間自動(dòng)機(jī)理論，應(yīng)用UPPAAL建模驗(yàn)證工具，對(duì)CTC分界口臨時(shí)限速的工作流程及信息交互過(guò)程進(jìn)行仿真建模，并對(duì)系統(tǒng)的安全性和受限活性進(jìn)行驗(yàn)證。

1 CTC分界口臨時(shí)限速場(chǎng)景分析

臨時(shí)限速系統(tǒng)的基本構(gòu)成如圖1所示。

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

臨時(shí)限速的設(shè)置應(yīng)滿足運(yùn)輸安全，并要求靈活設(shè)置。當(dāng)調(diào)度集中系統(tǒng)（CTC，Certralized Traffic Command System）分界口處由于施工、維修或自然災(zāi)害等原因需要設(shè)置臨時(shí)限速時(shí)，臨時(shí)限速系統(tǒng)不僅要完成自身臨時(shí)限速的設(shè)置，還要與相鄰調(diào)度臺(tái)臨時(shí)限速設(shè)備之間進(jìn)行信息交互。臨時(shí)限速在CTC分界口處的場(chǎng)景如圖2所示。

圖2 CTC分界口處臨時(shí)限速場(chǎng)景

其中，左側(cè)調(diào)度臺(tái)命名為A,右側(cè)調(diào)度臺(tái)命名為B，對(duì)應(yīng)設(shè)備均通過(guò)在其后面加上相應(yīng)的字母來(lái)區(qū)分。根據(jù)站場(chǎng)圖，標(biāo)示出相鄰調(diào)度臺(tái)臨時(shí)限速命令的擬定范圍和限速數(shù)據(jù)的覆蓋區(qū)域，并標(biāo)示出邊界TCC/RBC的單向臨時(shí)限速數(shù)據(jù)覆蓋區(qū)域（圖中范圍均為示意圖）。

根據(jù)圖2中的方向所示，臨時(shí)限速命令的擬定責(zé)任方遵循“以線路正方向，限速起點(diǎn)所在局”的歸屬原則。圖2中限速區(qū)1由CTC-A負(fù)責(zé)擬定，限速區(qū)2由CTC-B負(fù)責(zé)擬定，限速區(qū)1與限速區(qū)2均在兩側(cè)TSRS數(shù)據(jù)覆蓋范圍內(nèi)，因此，TSRS-A數(shù)據(jù)覆蓋區(qū)內(nèi)限速區(qū)1的限速信息要發(fā)送給TSRS-B，同時(shí)，TSRS-B臨時(shí)限速數(shù)據(jù)覆蓋區(qū)內(nèi)限速區(qū)2的數(shù)據(jù)也要發(fā)送給TSRS-A，使雙方的限速命令同步，這樣才能形成正式的臨時(shí)限速命令。當(dāng)出現(xiàn)通信中斷或其它原因照成命令狀態(tài)不一致，各TSRS請(qǐng)求刷新，進(jìn)行命令狀態(tài)同步，同步原則以命令發(fā)起方為準(zhǔn)。若同步失敗，則判斷為故障，跨界臨時(shí)限速設(shè)置不成功。各TSRS根據(jù)雙方的限速結(jié)果，生成最終的限速命令。

本論文主要對(duì)分界口臨時(shí)限速的擬定校驗(yàn)、驗(yàn)證、執(zhí)行流程進(jìn)行建模，由于臨時(shí)限速的取消流程與執(zhí)行流程類似，不再詳細(xì)分析其工作過(guò)程。

1.1 分界口臨時(shí)限速命令擬定

調(diào)度臺(tái)CTC-A施工調(diào)度員負(fù)責(zé)提出跨界臨時(shí)限速命令的申請(qǐng)，與相鄰的調(diào)度臺(tái)CTC-B聯(lián)系確認(rèn)后，擬定正式限速調(diào)度命令，下發(fā)給對(duì)應(yīng)的TSRS-A進(jìn)行有效性驗(yàn)證，并將驗(yàn)證結(jié)果傳遞給相鄰的TSRS-B，請(qǐng)求CTC-B的TSR校驗(yàn)，綜合兩側(cè)的校驗(yàn)結(jié)果，形成文本形式臨時(shí)限速調(diào)度命令，送至行調(diào)臺(tái)CTC-A、CTC-B，調(diào)度員確認(rèn)后存入TSRS。

1.2 分界口臨時(shí)限速命令激活驗(yàn)證

臨時(shí)限速服務(wù)器TSRS-A實(shí)時(shí)檢查存儲(chǔ)的臨時(shí)限速調(diào)度命令開(kāi)始執(zhí)行的時(shí)間，在計(jì)劃開(kāi)始執(zhí)行前30 min向原擬定方提示激活存儲(chǔ)的相應(yīng)臨時(shí)限速命令，并且每間隔10 min提示一次，直到確認(rèn)或超出命令結(jié)束時(shí)間。TSRS-A激活提示檢驗(yàn)通過(guò)后請(qǐng)求TSRS-B激活提示并檢驗(yàn)（除時(shí)間信息處，其它條件均滿足即可）。激活成功后由TSRS-A下達(dá)驗(yàn)證，并分發(fā)給相關(guān)TCC/RBC進(jìn)行驗(yàn)證，同時(shí)請(qǐng)求TSRS-B分發(fā)并進(jìn)行驗(yàn)證。

1.3 分界口臨時(shí)限速命令執(zhí)行

臨時(shí)限速服務(wù)器TSRS-A設(shè)置提示成功，請(qǐng)求TSRS-B設(shè)置提示，TSRS-A綜合設(shè)置提示結(jié)果，提示調(diào)度員下達(dá)執(zhí)行。TSRS-A分發(fā)限速命令至相關(guān)的TCC/RBC及TSRS-B執(zhí)行，TSRS-A在請(qǐng)求鄰站執(zhí)行結(jié)果的同時(shí)，告知本地執(zhí)行的中間結(jié)果，綜合執(zhí)行的結(jié)果并送行調(diào)臺(tái)顯示。

2 系統(tǒng)建模仿真

2.1 時(shí)間自動(dòng)機(jī)

時(shí)間自動(dòng)機(jī)使用時(shí)鐘變量表示時(shí)間，用一個(gè)約束條件來(lái)注釋狀態(tài)轉(zhuǎn)換圖，這個(gè)與時(shí)間有關(guān)的約束條件決定了狀態(tài)轉(zhuǎn)換的發(fā)生時(shí)機(jī)[2]。對(duì)于一個(gè)時(shí)鐘變量的有窮集合X，時(shí)鐘約束的集合φ(X)的形式語(yǔ)法為：φ：x≤c|c≤x|x

時(shí)間自動(dòng)機(jī)A是一個(gè)六元組（∑, S, S0, X, I,E），其中：∑ 是一個(gè)有窮標(biāo)記集合，S是一個(gè)有限狀態(tài)集合， S0∈S是開(kāi)始狀態(tài)集合，X是一個(gè)有限時(shí)鐘集合，I是一個(gè)映射，為每個(gè)位置s指定φ(X)中的一些時(shí)鐘約束，E?S×∑×2X×φ(X)×S是轉(zhuǎn)換集合，一個(gè)轉(zhuǎn)換（s, s', a, λ, φ)表示在符號(hào)a下從位置s到位置s'的一條邊，φ是X上的一個(gè)時(shí)鐘約束，指定什么時(shí)候轉(zhuǎn)換發(fā)生，集合λ?X指這次轉(zhuǎn)換中被復(fù)位的時(shí)鐘。時(shí)間自動(dòng)機(jī)的語(yǔ)義由一個(gè)與它相關(guān)的狀態(tài)轉(zhuǎn)換SA來(lái)定義，SA的一個(gè)狀態(tài)是一個(gè)偶對(duì)（s, v），s是A的一個(gè)位置，v是X的一個(gè)時(shí)鐘約束[3]。

2.2 基于時(shí)間自動(dòng)機(jī)模型

根據(jù)分界口臨時(shí)限速系統(tǒng)的工作流程，利用UPPAAL建模仿真工具建立時(shí)間自動(dòng)機(jī)模型。分界口臨時(shí)限速信息交互通過(guò)4個(gè)活動(dòng)對(duì)象來(lái)完成，即CTC-A、TSRS-A、TSRS-B 、CTC-B，構(gòu)造出每個(gè)對(duì)象的時(shí)間自動(dòng)機(jī)模型，通過(guò)自動(dòng)機(jī)網(wǎng)絡(luò)描述整個(gè)系統(tǒng)。構(gòu)造出時(shí)間自動(dòng)機(jī)依次記作 TACTC–A、TATSRS–A、TATSRS–B、TACTC–B，如圖3所示。

圖3 時(shí)間自動(dòng)機(jī)模型

圖3中，各位置之間通過(guò)同步通道實(shí)現(xiàn)轉(zhuǎn)換的同步發(fā)生，其中，“！”結(jié)尾的標(biāo)記表示發(fā)出此信號(hào)時(shí)轉(zhuǎn)換發(fā)生，“？”結(jié)尾的標(biāo)記表示接收到此信號(hào)時(shí)轉(zhuǎn)換發(fā)生[4]。標(biāo)有 C 的圓圈為堅(jiān)定位置[5]，可以凍結(jié)時(shí)間即下一個(gè)轉(zhuǎn)換必須無(wú)延遲的離開(kāi)。規(guī)定模型中位置的命名規(guī)則：各設(shè)備模型中以“P_”開(kāi)頭表示限速命令擬定(prepare)過(guò)程,以“E_”開(kāi)頭表示TSRS中限速命令的執(zhí)行下達(dá)（execute）過(guò)程，以“S_”開(kāi)頭表示限速命令的設(shè)置（set）過(guò)程。模型中的主要位置如表1所示。

表1 模型中的主要位置

模型中的主要通道如表2所示。

TA=TACTC–A||TATSRS–A||TACTC–B||TATSRS–B

整個(gè)時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)使用全局變量進(jìn)行通信，用來(lái)保證系統(tǒng)邏輯功能的準(zhǔn)確性。整型變量如confirmFlag、promptFlag、exeFlag分別用于控制確認(rèn)、提示、執(zhí)行結(jié)果，取值為1表示成功，0表示失敗，以此來(lái)達(dá)到模型邏輯的準(zhǔn)確性。應(yīng)用時(shí)鐘變量進(jìn)行精確的時(shí)鐘控制，設(shè)置時(shí)鐘集合 X={T0, T1, T2}，其中，T0用來(lái)控制分界口臨時(shí)限速命令激活驗(yàn)證提示時(shí)間，T1、T2用來(lái)描述相應(yīng)的TSRS與TCC/RBC的通信時(shí)間。模型中T_reaction、T_timeout分別表示TSRS與TCC/RBC通信的響應(yīng)時(shí)間和中斷時(shí)間，由于本文主要對(duì)分界口臨時(shí)限速系統(tǒng)信息交互進(jìn)行建模，側(cè)重于跨界限速，因此沒(méi)有列出TCC/RBC的時(shí)間自動(dòng)機(jī)模型，但在TSRS-A的模型中描述出了其與TCC/RBC的通信過(guò)程，同時(shí)，詳細(xì)對(duì)調(diào)度臺(tái)A限速命令的擬定、驗(yàn)證、下達(dá)過(guò)程進(jìn)行建模，與調(diào)度臺(tái)B有關(guān)的模型描述了輔助完成調(diào)度臺(tái)A限速命令下達(dá)的過(guò)程，其與調(diào)度臺(tái)A相似的工作過(guò)程，在模型中均省略。

3 系統(tǒng)模型驗(yàn)證

根據(jù)CTC分界口臨時(shí)限速系統(tǒng)約束提出的系統(tǒng)功能和性能要求，利用UPPAAL工具分別對(duì)其進(jìn)行驗(yàn)證，從而說(shuō)明系統(tǒng)的安全性和受限活性。

系統(tǒng)的安全性用于描述系統(tǒng)不一定發(fā)生的事情，指“壞的事情永遠(yuǎn)都不會(huì)發(fā)生”，其驗(yàn)證可以歸結(jié)為時(shí)間自動(dòng)機(jī)的可達(dá)性分析；系統(tǒng)的受限活性用于說(shuō)明系統(tǒng)必定會(huì)發(fā)生某些事情，指“好的事情終究會(huì)發(fā)生”[5]，可以由時(shí)間自動(dòng)機(jī)位置的不變式和轉(zhuǎn)換的約束條件來(lái)保證。

系統(tǒng)的功能和性能要求如下：

（1）功能屬性要求：a.CTC應(yīng)能擬定、設(shè)置、取消臨時(shí)限速命令；b.TSRS保證限速命令先驗(yàn)證后執(zhí)行；c.TSRS-A激活提示成功的同時(shí)請(qǐng)求相鄰TSRS-B激活提示；d.TSRS-A能分發(fā)臨時(shí)限速命令到相應(yīng)的TCC/RBC執(zhí)行同時(shí)請(qǐng)求TSRS-B分發(fā)執(zhí)行； e.各設(shè)備均應(yīng)對(duì)接收到的限速信息進(jìn)行有效性驗(yàn)證。

（2）性能屬性要求：a.TSRS-A通信響應(yīng)間隔在T_reaction內(nèi)完成；b.在T_timeout時(shí)間內(nèi)TSRS-A通信未完成， 則視為通信中斷。

UPPAAL為驗(yàn)證提供了一種BNF（Bac-kus Naur Form）語(yǔ)法：

Prop:= A[]φ|E<>φ|E[]φ|A<> →ψ其中φ,ψ為所驗(yàn)證的系統(tǒng)性質(zhì)的邏輯表達(dá)式；字符A、E用來(lái)量化路徑即時(shí)間自動(dòng)機(jī)描述的一個(gè)轉(zhuǎn)換，A表示給定的性質(zhì)對(duì)于所有路徑均滿足，E表示至少有一條路徑滿足性質(zhì)，[]、<>用來(lái)量化路徑上的狀態(tài)，[]表示路徑上的所有狀態(tài)均滿足給定的性質(zhì)，<>表示路徑上至少有一個(gè)狀態(tài)滿足給定的性質(zhì)。

應(yīng)用BNF語(yǔ)言在UPPAAL驗(yàn)證器中對(duì)以上列出的性質(zhì)進(jìn)行驗(yàn)證。

把上述驗(yàn)證語(yǔ)句輸入U(xiǎn)PPAAL驗(yàn)證器中，逐條驗(yàn)證每條性質(zhì)。

在驗(yàn)證器中，性質(zhì)列表中每條性質(zhì)后面的灰色圓形標(biāo)志變成綠色表示驗(yàn)證通過(guò)，驗(yàn)證的進(jìn)度與結(jié)果一欄中進(jìn)一步表明列表中所列的性質(zhì)均滿足，即CTC分界口臨時(shí)限速時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò) 能滿足系統(tǒng)的這些性質(zhì)。通過(guò)驗(yàn)證說(shuō)明模型是安全可靠的，系統(tǒng)滿足邏輯和時(shí)間上的要求。

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

本文在分析CTC調(diào)度臺(tái)分界口處臨時(shí)限速工作流程的基礎(chǔ)上，以其安全性和受限活性為驗(yàn)證目標(biāo)，建立整個(gè)系統(tǒng)交互的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型，作為驗(yàn)證的基礎(chǔ)。根據(jù)CTC分界口臨時(shí)限速系統(tǒng)約束提出功能和性能等系統(tǒng)性質(zhì)，利用UPPAAL驗(yàn)證工具，驗(yàn)證了各條性質(zhì)均得到滿足，從而說(shuō)明了系統(tǒng)的安全性和受限活性，為系統(tǒng)的設(shè)計(jì)和開(kāi)發(fā)提供了一定的依據(jù)。

[1]古天龍.軟件開(kāi)發(fā)的形式化方法[M].北京:高等教育出版社，2005：5-67.

[2]吳永剛，陸慧娟.基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)建模及驗(yàn)證[J].計(jì)算機(jī)時(shí)代，20116（1）：2-3.

[3]劉傳會(huì)，張廣泉.一種基于時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)的實(shí)時(shí)系統(tǒng)形式化驗(yàn)證方法[J].蘇州大學(xué)學(xué)報(bào)，2008，24（1）：35-40.

[4]袁 磊，王俊峰.CTCS-3級(jí)列控系統(tǒng)臨時(shí)限速建模與驗(yàn)證[J].西南交通大學(xué)學(xué)報(bào)，2013，48（4）：710-712.

[5]OLDEROGER, DIERKSH. Real-time systems[M].London:Cambridge University Press，2008: 137-146．

[6]康仁偉.基于時(shí)間自動(dòng)機(jī)的CTCS-3級(jí)列控系統(tǒng)建模方法與驗(yàn)證研究[D].北京:北京交通大學(xué)， 2013：40-53.