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

1 引言

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

該聯(lián)鎖系統(tǒng)進路控制功能通過模塊間頻繁的通信來實現(xiàn)，有較強的時間約束，屬于復雜實時系統(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)絡層和邏輯控制層組成。將傳統(tǒng)集中聯(lián)鎖邏輯功能分散到各個電子模塊，通過電子模塊相互協(xié)作完成進路的建立和解鎖（如圖1 所示）。

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

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

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

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

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

圖2 站場圖

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

（1）選排階段

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

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

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

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

（2）進路鎖閉

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

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

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

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

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

（3）信號開放

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

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

（4）信號開放保持

①X 檢查燈絲的完好性。

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

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

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

（5）進路解鎖

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

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

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

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

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

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

2.2 時間自動機模型

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

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

2.3 模型分析驗證

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

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

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

3 總結(jié)

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

[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]于飛.分散控制計算機聯(lián)鎖系統(tǒng)網(wǎng)絡通信研究[D].西南交通大學.2012.

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

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