軌道交通聯鎖領域特定語言的形式化

仇楊杰

摘 要：聯鎖系統是軌道交通系統的核心子系統之一，其安全和穩定對軌道交通的運行有重要的價值，所以在實踐中需要關注聯鎖系統的安全分析與加強。在現階段的工作實踐中，利用形式化建模和分析的方法對聯鎖系統進行分析研究是保障系統安全的重要手段，所以做好形式化建模的分析與討論。在形式化建設分析實踐中需要領域知識和形式化知識結合，而要真正地實現兩種知識的結合，需要在實踐中針對領域進行特定語言的形式化。這樣，生成的模型才會更具指向性，相關分析工作的專業性、規范性表現也會更加的突出。文章對軌道交通聯鎖領域特定語言的形式化做分析，旨在指導實踐工作。

關鍵詞：軌道交通;特定語言;形式化

對軌道交通聯鎖系統做具體的分析會發現其作為軌道交通的核心子系統之一，在實踐中發揮著重要的作用，所以強調軌道交通聯鎖系統的研究與分析有非常突出的現實意義。對聯鎖系統的具體運行來看，其主要的技術手段有計算機、現代多媒體以及網絡通信等。該系統涉及的設備比較多，與之相關的聯鎖關系也比較多，所以如果該系統存在問題，那么整個軌道交通的運行安全等會大打折扣。為了實現軌道交通安全運行，對聯鎖系統的安全性做強調意義顯著。利用形式化建模的方式做相應的分析，分析結果準確性更加突出，需要注意的是在建模的過程中需要使用特定語言，而且語言要符合形式化的要求?；诖?，對軌道交通聯鎖設備特定語言形式化做分析與討論便有了突出的現實價值。

1預備知識

在聯鎖領域特定語言形式化過程中，預備知識是必不可少的，所以必須要基于特定領域語言形式化目標對需要掌握和利用的具體知識進行明確。對特定領域語言形式化做分析可知隨機混成自動機是一種被廣泛接受的混合系統模型，該模型還是建模時間和隨機性的重要模型，在目前的計算機仿真、自動機等領域得到了廣泛應用[1]。就隨機混成自動機的具體利用分析來看，其包含了隨機性，所以在引入隨機事件之后，非常合適以故障診斷為目的的建模，其和傳統的時間自動機進行比較有顯著的不同，即該種自動機所提供的是對離散行為、連續行為和隨機行為的描述，其能夠對存在隨機行為的混成系統進行很好的建模。

在實踐中，利用廣播信道和共享變量，不同的隨機混成自動機之間可以實現相互通信，進而組成隨機混成自動機網絡。對該網絡的具體狀態進行區分和利用，網絡應用效果會更加顯著。總的來講，在特定領域語言形式化過程中，隨機混成自動機是非常重要的應用內容，對該內容的具體應用情況和相關知識做總結與明確，可以使整體工作開展的預備知識更加完善。這樣，整體工作實效也會有顯著進步。

2方法框架

在明確了預備知識的基礎上對語言形式化的方法框架做討論與分析，這對于語言形式化實現幫助巨大。為了實現列車行車的安全性，聯鎖系統的首要目標是在允許列車移動的同時對道岔和信號燈進行控制，以此來規避列車發生碰撞或者是脫軌的情況?；诖?，聯鎖系統的主要功能必須要明確。在實踐中，其功能主要表現為通過軌道電路監視相關軌道段的占用情況，對道岔的位置踐行控制，并發送信號給列車司機，告知其能否進入到軌道。就具體的工作目標實施來看，其基本流程為 ：1）列車向控制器發送請求，申請進入相應道路并等待反饋。2）在接收到列車發出的請求信息后，控制器進行聯鎖表的查詢，并獲取進路結果。3）控制器對進路軌道的占用情況進行檢查，并獲取準確的軌道占用結果[2]。4）在檢查進路軌道結果獲取之后，控制器命令鎖閉道岔，同時指導道岔移動到相應的位置，道岔在移動完成之后向控制器反饋結果。5）控制器完成對道岔的控制后向信號燈發送變綠信號，并控制信號燈變綠。6）控制器在列車行駛出軌道后進行相應道岔的解鎖，然后控制相應的信號燈變紅。

基于上述的具體流程進行聯鎖系統模型的建設，一方面需要構建模型控制器，另一方面需要構建與控制器交互的環境。對環境中的具體內容進行明確，保證環境中設備的完整，同時對其做類別劃分，這樣，具體的建模會有更加準確、完善的資料。在資料明確的基礎上基于語言形式化的要求明確方法和相應的框架，這樣，最終的工作實施效果會更加突出。

3聯鎖領域特定語言IS-DSL

基于上述的具體分析，聯鎖系統的模型建設首先在構件數量上存在著明顯的差異，也就是說列車、道岔以及信號燈和軌道實體化的個數會隨著案例而出現明顯的變化。因為這些構件的數量是語言的重要組成部分，所以需要對這些構件的數量進行明確。不僅如此，因為實體數量的具體變化會導致進路表發生明顯的差異，因此在實踐中需要基于實際數量變化情況對進路表進行制定。

進路表是聯鎖控制的重要組成部分，而聯鎖表的具體表示也應該是領域特定語言的一部分[3]。在相關分析中發現：一個聯鎖表的主要組成部分是進路，而每個進路又包含了一系列的軌道，且軌道邊上還有信號燈以及道岔，所以可以將聯鎖表定義為一組進路。對每個進路的標識進行明確，同時明確進路的軌道序列，這樣，每段軌道可以使用軌道的表示符號。進入到該軌道之后吸納紅燈也要用相應的標識符號，至于道岔等也需要有相應的表述符號，這樣每一個進路便會有自身的特殊標識符號，改符號可以作為語言形式化的重要內容。簡單來講，語言形式化需要有明確的方法，在可續選用方法的基礎上實現語言的形式化，使特定領域的語言使用具有獨特性和代表性，這樣，語言表達的含義更加準確，內容具有唯一性，其在實踐中的應用效果顯著提升。

結束語：

綜上所述，軌道交通聯鎖領域特定語言的形式化對聯鎖控制實踐有突出的現實價值，所以在實踐中明確相應的工作內容，實現語言形式化現實意義顯著。文章對聯鎖領域特定語言形式化的具體步驟和方法做分析，目的是要為現階段的具體工作開展提供指導和幫助。

參考文獻：

[1]姜靖，鄭啟龍.面向計算機視覺的領域特定語言[J].小型微型計算機系統，2020，041（003）：617-624.

[2]曹祺.基于領域語言的圖書館檢索語言的優化[J].中國高新科技，2020，No.66（06）：48-53.

[3]常博.基于通信列車控制的計算機城市軌道交通聯鎖子系統功能測試研究[J]. 自動化技術與應用，2020，039（003）：166-169.

（蘇州市軌道交通集團有限公司運營一分公司，江蘇 蘇州 215000）