分散控制計算機聯鎖系統建模的研究

黃 菊 西南交通大學信息科學與技術學院

1 引言

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

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

2 分散控制計算機聯鎖系統的建模與驗證

2.1 分散控制計算機聯鎖系統

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

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

圖1 分散控制計算機聯鎖系統結構圖

通信網絡層完成操作層與邏輯控制層之間的通信，以及邏輯控制層電子模塊與電子模塊之間的通信。

邏輯控制層包括信號機電子模塊、道岔電子模塊和軌道電路電子模塊，每個模塊都是全電子模塊，相當于一臺微型計算機，完成聯鎖邏輯運算和現場信號設備的驅動采集功能。

被控設備層指現場設備，包括信號機、道岔和軌道區段。它們在物理上完成聯鎖邏輯命令，實現車站聯鎖功能。以站場圖（見圖2）舉例分析分散控制計算機聯鎖系統進路控制過程。

圖2 站場圖

調度員通過終端操作機先后按壓XLA 信號按鈕和S3LA信號按鈕。操作層對進路進行合法性檢查，通過靜態聯鎖表查找到始端信號機ID 號，將進路命令發送到始端信號機電子模塊。

（1）選排階段

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

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

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

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

（2）進路鎖閉

①X 發送鎖閉命令，等待鎖閉信息回復。

②D1、D5 和S3 接收命令，再次檢查鎖閉條件，設置進程標志，返回鎖閉信息。

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

④ⅠAG、1DG、5DG 和3G 接收命令，再次檢查區段鎖閉條件，設置鎖閉標志，返回鎖閉信息。

⑤X 在規定時間內根據電子模塊返回的鎖閉信息后，判斷進路是否鎖閉，設置進程標志。

（3）信號開放

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

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

（4）信號開放保持

①X 檢查燈絲的完好性。

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

③當列車進入ⅠAG 時，區段將信息發送給X，X 立即關閉信號。

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

（5）進路解鎖

①X 正常關閉后，發送解鎖命令，等待解鎖信息回復。

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

③D1、D5 和S3 接收解鎖命令，設置進程標志，消亡進路對本模塊的占用，返回解鎖信息。

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

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

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

2.2 時間自動機模型

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

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

2.3 模型分析驗證

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

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

圖4 進路選排的仿真時序圖

3 總結

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

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

[2]王靜.基于時間自動機的模型驗證理論及應用研究[D].鄭州大學.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]于飛.分散控制計算機聯鎖系統網絡通信研究[D].西南交通大學.2012.

[7]陳曉偉.新型分布式計算機聯鎖系統的研究與設計[D].蘭州交通大學,2009.

[8]王觀寧.基于UPPAAL 的聯鎖進路控制流程建模與驗證[D].北京交通大學.2009.