基于時間自動機(jī)的列控系統(tǒng)等級轉(zhuǎn)換建模與驗證

董家希，劉珂帆，鄢春花，杜利芳，周家宇

（成都工業(yè)學(xué)院 汽車與交通學(xué)院，四川 成都）

引言

在列車運行過程中，需要十分嚴(yán)苛復(fù)雜的控制系統(tǒng)對于其安全穩(wěn)定運行起到保障作用。等級轉(zhuǎn)換作為列控系統(tǒng)中的重要組成部分，每個環(huán)節(jié)的運作都必須得到嚴(yán)格的檢查和確認(rèn)，方能順利推進(jìn)。近年來，對于列控系統(tǒng)進(jìn)行形式化建模，取得了豐碩的成果。其中，基于時間自動機(jī)原理的模型能夠?qū)?fù)雜抽象的列控系統(tǒng)等級轉(zhuǎn)換過程更加直觀、全面、清晰的呈現(xiàn)出來，因此在實時系統(tǒng)問題的研究中具備良好的表現(xiàn)[1]。

1 時間自動機(jī)模型

1.1 時間自動機(jī)理論

時間自動機(jī)(Timed Automata, TA)是一種面向?qū)崟r系統(tǒng)進(jìn)行建模和驗證分析的理論，為具有時間特征的系統(tǒng)的狀態(tài)轉(zhuǎn)換圖的描述提供了一種簡潔有效的方法[2]。

時間自動機(jī)系統(tǒng)將復(fù)雜的實時系統(tǒng)抽象為狀態(tài)和邊的轉(zhuǎn)換關(guān)系，并為其轉(zhuǎn)移條件提供了相應(yīng)的時鐘約束，每個狀態(tài)改變都可以配合觸發(fā)啟動對應(yīng)的時鐘計時模式，這個時鐘約束所對應(yīng)的轉(zhuǎn)移條件在滿足時鐘約束的條件下才能夠執(zhí)行。

時間約束的集合(X)的定義如下：

其中，X 表示時鐘變量，x 表示其中一個時鐘，時鐘解釋表示為時鐘集X 上的每一個時鐘賦予的一個實數(shù)值。

其中，T?R+，Tx為X 上所有時鐘解釋的集合。

在一個復(fù)雜的實時系統(tǒng)中，常常是由多個子系統(tǒng)構(gòu)成的，他們之間相互獨立又彼此配合，頻繁進(jìn)行子系統(tǒng)之間的信息交互，保證整個系統(tǒng)的協(xié)同合作，從而完成復(fù)雜實時系統(tǒng)對應(yīng)的功能。因此我們可以用組成該系統(tǒng)的各個子系統(tǒng)的積來描述系統(tǒng)的功能，稱為時間自動機(jī)的積[3]。

設(shè)兩個時間自動機(jī)TA1=，TA2=，時鐘集合X1和X2不相交，則TA1和TA2的積記為TA1|| TA2。

1.2 UPPAAL 建模

UPPAAL 軟件采用圖形化的界面，主要由四個部分組成[4]。System Editor 是用于創(chuàng)建實時系統(tǒng)建模的工具。Simulator 是建模的初始步驟，它以圖形方式表示系統(tǒng)的邏輯關(guān)系。Verifier 則是實現(xiàn)系統(tǒng)功能仿真和時序仿真的關(guān)鍵工具。在設(shè)計階段Verifier 可以檢查所有可能的執(zhí)行路徑，并在驗證之前對已有模型進(jìn)行檢驗。Yggdrasil則用于測試用例的自動生成，可進(jìn)行深度搜索，分析其測試用例覆蓋的運營場景，還可以根據(jù)所驗證性質(zhì)進(jìn)行測試用例的自動生成。UPPAAL 結(jié)構(gòu)體系見圖1。

圖1 UPPAAL結(jié)構(gòu)體系

TA 模型包括狀態(tài)、邊和約束條件三個元素。在TA模型中，兩個子系統(tǒng)之間的信息交互通過通道完成。UPPAAL 中所支持的BNF 語法主要有4 種表現(xiàn)方式[5]，其BNF 語句及含義見表1。

表1 BNF 語句及含義

2 等級轉(zhuǎn)換場景需求分析

2.1 等級轉(zhuǎn)換場景過程分析

當(dāng)列車進(jìn)行C2 到C3 等級轉(zhuǎn)換時，邊界上設(shè)置了應(yīng)答器、轉(zhuǎn)換點以及司機(jī)確認(rèn)區(qū)等，具體布置見圖2。

圖2 等級轉(zhuǎn)換邊界布置示意

2.2 建立等級轉(zhuǎn)換信息交互圖

將C2 至C3 列控系統(tǒng)等級轉(zhuǎn)換流程場景抽象描述為司機(jī)、應(yīng)答器、車載設(shè)備和RBC 四個子系統(tǒng)之間的信息交互過程。它們通過傳輸包含不同指令的信息包來進(jìn)行信息的傳遞。

對于根據(jù)需求規(guī)范歸納出來的C2 至C3 列控系統(tǒng)等級轉(zhuǎn)換流程的描述，繪制了C2 至C3 級列控系統(tǒng)等級轉(zhuǎn)換流程信息交互序列圖見圖3。

圖3 等級轉(zhuǎn)換流程信息交互序列圖

3 等級轉(zhuǎn)換場景建模與驗證

在構(gòu)建模型時，我們將整個系統(tǒng)劃分為Train、Balise、RBC 和Driver 四個子系統(tǒng)，并分別構(gòu)建這些子系統(tǒng)的UPPAAL 模型。

3.1 等級轉(zhuǎn)換場景建模

在等級轉(zhuǎn)換場景建模中，車載子系統(tǒng)是其中最復(fù)雜的部分。當(dāng)列車通過等級轉(zhuǎn)換區(qū)域時，車載子系統(tǒng)根據(jù)列車實時狀態(tài)，頻繁地與應(yīng)答器、RBC 以及司機(jī)界面進(jìn)行信息傳遞，以確保等級轉(zhuǎn)換順利進(jìn)行。等級轉(zhuǎn)換Train子系統(tǒng)模型見圖4。

應(yīng)答器子系統(tǒng)作為車地信息交互的渠道，用于判斷列車位置，根據(jù)需求不同設(shè)置的相應(yīng)功能的應(yīng)答器，可以實現(xiàn)列車定位，為等級轉(zhuǎn)換提供位置信息。等級轉(zhuǎn)換Balise 子系統(tǒng)模型見圖5。

圖5 等級轉(zhuǎn)換Balise 子系統(tǒng)模型

RBC 根據(jù)收到信息生成控制命令，提供行車許可，保證列車運行安全性，模型見圖6。

圖6 等級轉(zhuǎn)換RBC 子系統(tǒng)模型

當(dāng)接收到RBC 傳送的等級轉(zhuǎn)換命令后，車載設(shè)備就會向司機(jī)發(fā)送等級轉(zhuǎn)換確認(rèn)請求，司機(jī)通過按壓按鈕對于等級轉(zhuǎn)換過程進(jìn)行確認(rèn)。這樣可以通過自動化操作和人工操作兩個方面來完整地驗證列控系統(tǒng)等級轉(zhuǎn)換的條件，實現(xiàn)雙保險。等級轉(zhuǎn)換Driver 子系統(tǒng)模型見圖7。

圖7 等級轉(zhuǎn)換Driver 子系統(tǒng)模型

3.2 等級轉(zhuǎn)換場景模型驗證

得到狀態(tài)轉(zhuǎn)移圖后，還需要運用UPPAAL 的驗證器對模型進(jìn)行進(jìn)一步的驗證，保證模型的正確性。利用形式化驗證的方法確保模型滿足系統(tǒng)的功能性需求和實時性需求，其流程見圖8。

圖8 基于UPPAAL的形式化驗證流程

功能性要求主要關(guān)注研究所建立的模型對于轉(zhuǎn)換流程的完整性。例如，確保系統(tǒng)能夠按照實際流程順利完成所需的步驟，防止系統(tǒng)出現(xiàn)死鎖，并確保執(zhí)行操作能夠正常進(jìn)行。同時，在設(shè)備正常運行的情況下，系統(tǒng)應(yīng)能夠?qū)崿F(xiàn)從C2 級到C3 級列控系統(tǒng)的等級轉(zhuǎn)換。當(dāng)轉(zhuǎn)換條件不滿足時，系統(tǒng)應(yīng)能夠保持C2 級列控系統(tǒng)的控車運行等。等級轉(zhuǎn)換功能性要求驗證運行結(jié)果見圖9。

圖9 等級轉(zhuǎn)換功能性要求驗證結(jié)果

實時性要求主要驗證系統(tǒng)的時間特性。等級轉(zhuǎn)換場景對時間的要求十分嚴(yán)格，因此，模型中狀態(tài)遷移的時間約束能否有效合理進(jìn)行是模型建立成功與否的關(guān)鍵因素。等級轉(zhuǎn)換實時性要求驗證運行結(jié)果見圖10。

圖10 等級轉(zhuǎn)換實時性要求驗證結(jié)果

經(jīng)過等級轉(zhuǎn)換過程中對每條性質(zhì)的逐一驗證，得出的驗證結(jié)果發(fā)現(xiàn)每條性質(zhì)均是可達(dá)的，說明系統(tǒng)可以滿足相應(yīng)的性能和需求，證明所建立的時間自動機(jī)模型是安全可靠的。

4 結(jié)論

本文提出了一種基于模型對于復(fù)雜實時系統(tǒng)的研究方法，并對模型的準(zhǔn)確性及完備性進(jìn)行形式化驗證。首先，對于列控系統(tǒng)的等級轉(zhuǎn)換場景進(jìn)行過程性分析和提取需求，梳理各子系統(tǒng)之間的信息交互流程。其次，基于時間自動機(jī)原理，借助UPPAAL 建模工具，建立四個子系統(tǒng)的狀態(tài)轉(zhuǎn)移圖模型。最后，對標(biāo)列控系統(tǒng)規(guī)范要求，結(jié)合BNF 邏輯公式和系統(tǒng)驗證器，對于模型的實時性和功能性需求給出驗證，保證了此模型的準(zhǔn)確性和可靠性。對于基于模型的研究問題具有一定的借鑒意義。