分散控制計算機聯(lián)鎖系統(tǒng)建模的研究

黃 菊 西南交通大學(xué)信息科學(xué)與技術(shù)學(xué)院

1 引言

聯(lián)鎖控制系統(tǒng)是保證列車安全運行的關(guān)鍵技術(shù)。目前普遍采用的聯(lián)鎖系統(tǒng)屬于集中控制聯(lián)鎖系統(tǒng)，邏輯運算由聯(lián)鎖主機完成，聯(lián)鎖主機故障將導(dǎo)致整個系統(tǒng)無法運行。如果站場改造，邏輯聯(lián)鎖關(guān)系發(fā)生改變必須停止整個運行的聯(lián)鎖系統(tǒng)來修改聯(lián)鎖表，影響運輸效率。為了滿足越來越復(fù)雜的站場結(jié)構(gòu)以及要提高鐵路運輸效率的要求，近年來提出了具有更高可靠性的分散控制計算機聯(lián)鎖系統(tǒng)[5,6,7]。該系統(tǒng)取消了聯(lián)鎖主機，基于全電子技術(shù)以信號機、道岔和軌道電路區(qū)段為基本單位分別設(shè)置對應(yīng)的電子模塊單元，通過這些電子模塊相互協(xié)作完成進(jìn)路聯(lián)鎖邏輯運算控制。目前國內(nèi)外仍然處于理論研究階段，沒有實際應(yīng)用。

該聯(lián)鎖系統(tǒng)進(jìn)路控制功能通過模塊間頻繁的通信來實現(xiàn)，有較強的時間約束，屬于復(fù)雜實時系統(tǒng)。該系統(tǒng)建模采用基于時間自動理論的模型驗證工具UPPAAL，通過仿真時序圖分析系統(tǒng)信息交換情況，驗證系統(tǒng)功能特性、安全性和時間特性。

2 分散控制計算機聯(lián)鎖系統(tǒng)的建模與驗證

2.1 分散控制計算機聯(lián)鎖系統(tǒng)

分散控制計算機聯(lián)鎖系統(tǒng)也可叫分布式計算機聯(lián)鎖系統(tǒng)[6,7]，是相對于目前集中控制聯(lián)鎖系統(tǒng)而提出的一種全新概念。它由操作表示層、通信網(wǎng)絡(luò)層和邏輯控制層組成。將傳統(tǒng)集中聯(lián)鎖邏輯功能分散到各個電子模塊，通過電子模塊相互協(xié)作完成進(jìn)路的建立和解鎖（如圖1 所示）。

操作表示層[6]是人機交互的界面。負(fù)責(zé)實時顯示站場設(shè)備狀態(tài)、操作狀態(tài)和各類電子模塊的狀態(tài)；完成調(diào)度命令輸入，形成操作指令并發(fā)送到邏輯控制層；此外還包含文字和語音的操作提示。維修機相當(dāng)于微機監(jiān)測系統(tǒng)，完成系統(tǒng)的監(jiān)視功能，實時記錄設(shè)備運行情況，包括來自上位機的操作信息、邏輯控制層的數(shù)據(jù)和故障信息等。

圖1 分散控制計算機聯(lián)鎖系統(tǒng)結(jié)構(gòu)圖

通信網(wǎng)絡(luò)層完成操作層與邏輯控制層之間的通信，以及邏輯控制層電子模塊與電子模塊之間的通信。

邏輯控制層包括信號機電子模塊、道岔電子模塊和軌道電路電子模塊，每個模塊都是全電子模塊，相當(dāng)于一臺微型計算機，完成聯(lián)鎖邏輯運算和現(xiàn)場信號設(shè)備的驅(qū)動采集功能。

被控設(shè)備層指現(xiàn)場設(shè)備，包括信號機、道岔和軌道區(qū)段。它們在物理上完成聯(lián)鎖邏輯命令，實現(xiàn)車站聯(lián)鎖功能。以站場圖（見圖2）舉例分析分散控制計算機聯(lián)鎖系統(tǒng)進(jìn)路控制過程。

圖2 站場圖

調(diào)度員通過終端操作機先后按壓XLA 信號按鈕和S3LA信號按鈕。操作層對進(jìn)路進(jìn)行合法性檢查，通過靜態(tài)聯(lián)鎖表查找到始端信號機ID 號，將進(jìn)路命令發(fā)送到始端信號機電子模塊。

（1）選排階段

①X 接收進(jìn)路命令后，判斷本信號機是否空閑，是否被征用或者故障，滿足條件，根據(jù)進(jìn)路號查找聯(lián)鎖表中參與進(jìn)路的電子模塊信息，將進(jìn)路選排命令發(fā)送給參與進(jìn)路的電子模塊，等待模塊回復(fù)信息，在一定時間內(nèi)根據(jù)回復(fù)的信息進(jìn)行聯(lián)鎖邏輯判斷。

②C1 和C5 接收進(jìn)路選排命令，判斷道岔是否鎖閉，是否參與其它進(jìn)路控制，滿足條件將進(jìn)路要求的道岔位置與采集道岔狀態(tài)比較。道岔在規(guī)定位置，回復(fù)始端信號機道岔滿足條件；如果不在規(guī)定位置，生成道岔控制命令，在規(guī)定時間內(nèi)道岔轉(zhuǎn)換到規(guī)定位置將信息返回始端信號機，否則將失敗信息返回始端信號機。

③D1、D5 和S3 作為敵對信號接收到進(jìn)路選排命令，檢查是否已被征用或者故障，回復(fù)始端信號機敵對信號情況。

④ⅠAG、1DG、5DG 和3G 軌道區(qū)段電子模塊接收進(jìn)路選排命令，檢查區(qū)段是否參與其它進(jìn)路控制、是否鎖閉、是否空閑，回復(fù)始端信號機軌道區(qū)段情況。

（2）進(jìn)路鎖閉

①X 發(fā)送鎖閉命令，等待鎖閉信息回復(fù)。

②D1、D5 和S3 接收命令，再次檢查鎖閉條件，設(shè)置進(jìn)程標(biāo)志，返回鎖閉信息。

③C1 和C5 接收命令，再次檢查道岔鎖閉條件，設(shè)置鎖閉標(biāo)志，返回鎖閉信息。

④ⅠAG、1DG、5DG 和3G 接收命令，再次檢查區(qū)段鎖閉條件，設(shè)置鎖閉標(biāo)志，返回鎖閉信息。

⑤X 在規(guī)定時間內(nèi)根據(jù)電子模塊返回的鎖閉信息后，判斷進(jìn)路是否鎖閉，設(shè)置進(jìn)程標(biāo)志。

（3）信號開放

①X 檢查信號機燈絲是否故障，發(fā)送信號開放檢查命令，等待信號開放條件回復(fù)。

②ⅠAG、D1、C1、1DG、D5、C5、5DG、S3 和3G 再次檢查信號開放的條件，回復(fù)X 檢查結(jié)果，X 根據(jù)檢查結(jié)果，判斷開放條件是否成立，生成信號開放的驅(qū)動命令。

（4）信號開放保持

①X 檢查燈絲的完好性。

②X 與ⅠAG、D1、C1、1DG、D5、C5、5DG、S3 和3G 保持通信，檢查信號開放的條件，并獲得列車占用信息。

③當(dāng)列車進(jìn)入ⅠAG 時，區(qū)段將信息發(fā)送給X，X 立即關(guān)閉信號。

④如果有列車越過了ⅠAG，直接進(jìn)入1DG 或者5DG 或者3G，返回故障，關(guān)閉信號。

（5）進(jìn)路解鎖

①X 正常關(guān)閉后，發(fā)送解鎖命令，等待解鎖信息回復(fù)。

②C1 接收解鎖命令，檢查1DG 是否已經(jīng)解鎖，接收到1DG 的解鎖信息，那么道岔可以解鎖，設(shè)置鎖閉標(biāo)志，消亡進(jìn)路對本模塊的占用，返回解鎖信息；C5 同理。

③D1、D5 和S3 接收解鎖命令，設(shè)置進(jìn)程標(biāo)志，消亡進(jìn)路對本模塊的占用，返回解鎖信息。

④ⅠAG、1DG、5DG 和3G 在接收解鎖命令，相互通信，得到列車占用出清情況，進(jìn)行解鎖條件的判斷。ⅠAG 滿足"兩點"檢查，1DG、5DG 和3G 滿足"三點"檢查，設(shè)置鎖閉標(biāo)志設(shè)置，消亡進(jìn)路對本模塊的占用，返回解鎖信息。

⑤X 在接收所有模塊的解鎖信息后，解鎖該進(jìn)路，消亡進(jìn)路對本信號機的占用。

通過以上分析，可見進(jìn)路控制過程的著力點在始端信號機電子模塊和參與該進(jìn)路的其它電子模塊，如果一個模塊故障，只影響與該模塊有關(guān)的進(jìn)路，并不影響站內(nèi)其它進(jìn)路，所以在一定程度上分散了故障點。

2.2 時間自動機模型

采用基于時間自動機理論[1,2]的UPPAAL[3,4,8]對系統(tǒng)進(jìn)行建模，該理論已經(jīng)很成熟，不再詳述。以下以一條列車接車進(jìn)路的進(jìn)路選排過程為例說明信號機、道岔、區(qū)段電子模塊之間的協(xié)作關(guān)系。對操作層、始端信號機、軌道區(qū)段、敵對信號和道岔電子模塊分別建立時間自動機模型（圖3 為操作層建立時間自動機模型，始端信號機、軌道區(qū)段、敵對信號和道岔電子模塊與圖3 類似）。

圖3 操作層時間自動機模型

2.3 模型分析驗證

模型建立后，在模擬器中隨機運行可得到仿真時序圖。通過仿真時序圖可觀察模塊之間信息的交互情況，如圖4 所示。

操作層與始端信號機在2 個時間單位內(nèi)通過Route_Com和Com_Reply 通信；始端信號機對進(jìn)路命令進(jìn)行處理后，在1個時間單位內(nèi)向道岔、軌道區(qū)段和對信號電子模塊發(fā)送CheckCom 選路檢查命令；道岔、軌道區(qū)段和對信號電子模塊不管滿足選排條件與否都必須在2 個時間單位內(nèi)完成檢查并回復(fù)始端信號機檢查情況，分別通過SuccT、SuccSw、SuccCs 或者FailT、FailSw、FailCs 進(jìn)行信息交互。如果道岔位置不在規(guī)定位置，道岔電子模塊生成道岔驅(qū)動命令，通過SetTime啟動內(nèi)部時鐘，如果在13 個時間單位內(nèi)完成道岔的轉(zhuǎn)換，通過Reset 復(fù)位時鐘，反之道岔轉(zhuǎn)換失敗，進(jìn)行故障處理，發(fā)出TimeOut 時間溢出信息。同時在驗證器中使用屬性驗證語法可以對選排階段的功能性質(zhì)進(jìn)行驗證。如A[] not deadlock 通過驗證，表明模型不會出現(xiàn)死瑣；A<>Switch.ChangeSwitch imply SwPosNow==0 通過驗證，表明只有道岔位置不符合進(jìn)路要求位置時才會轉(zhuǎn)動道岔；A<>FirstSignal.count! =3 imply route==1 未通過驗證，表明有電子模塊不滿足選排條件，進(jìn)路選排失敗。其它性質(zhì)也可以通過邏輯公式進(jìn)行驗證，在此不詳述。

圖4 進(jìn)路選排的仿真時序圖

3 總結(jié)

本文介紹了分散控制計算機聯(lián)鎖系統(tǒng)的結(jié)構(gòu)及功能特點，用UPPAAL 對分散控制計算機聯(lián)鎖系統(tǒng)進(jìn)行建模。通過仿真時序圖分析了模塊之間的通信過程和狀態(tài)。進(jìn)路選排模型展現(xiàn)了信號機、道岔和軌道區(qū)段電子模塊在進(jìn)路控制中的協(xié)作關(guān)系。雖然驗證了分散控制計算機聯(lián)鎖系統(tǒng)的部分功能性質(zhì)，但后期還可以對系統(tǒng)進(jìn)一步深化，考慮更全面的進(jìn)路控制過程、更多的故障狀態(tài)和更多的電子模塊使模型更精準(zhǔn)，才能為分散控制計算機聯(lián)鎖軟件設(shè)計提供參考。

[1]R.Alur,D.L.Dill,A theory of timed automata.Journal of Theoretical Computer Science, 126(2):183-235,1994.

[2]王靜.基于時間自動機的模型驗證理論及應(yīng)用研究[D].鄭州大學(xué).2005.

[3]G.Behrmann,A.David,and K.Larsen.A tutorial on Uppaal.In Formal Methods for the Design of Real-Time Systems,Springer Verlag,2004,Lecture Notes in Computer Science,Vol.(3185):pages 200-236.

[4]http://www.uppaal.com/.

[5]Hei X,Takahashi S,Hideo N.Toward developing a Decentralized Railway Signalling System Using Petri Nets [C].Robotics, Automation and Mechatronics, 2008 IEEE Conference on. IEEE, 2008: Pages851-855.

[6]于飛.分散控制計算機聯(lián)鎖系統(tǒng)網(wǎng)絡(luò)通信研究[D].西南交通大學(xué).2012.

[7]陳曉偉.新型分布式計算機聯(lián)鎖系統(tǒng)的研究與設(shè)計[D].蘭州交通大學(xué),2009.

[8]王觀寧.基于UPPAAL 的聯(lián)鎖進(jìn)路控制流程建模與驗證[D].北京交通大學(xué).2009.