基于時間自動機的分散控制聯(lián)鎖系統(tǒng)建模與驗證.pdf

1、在鐵路信號系統(tǒng)中，聯(lián)鎖系統(tǒng)是不可缺少的核心技術(shù)裝備，它通過技術(shù)方法實現(xiàn)車站管轄范圍內(nèi)的信號機、道岔和進路的制約關(guān)系，保證了站內(nèi)行車安全，提高了鐵路運輸效率。近年來隨著通信技術(shù)、控制技術(shù)和微電子技術(shù)的發(fā)展，提出了一種新型的聯(lián)鎖制式——分散控制聯(lián)鎖系統(tǒng)。
　　 分散控制聯(lián)鎖系統(tǒng)改變了傳統(tǒng)集中控制的聯(lián)鎖方式，利用獨立全電子模塊與現(xiàn)場信號設(shè)備一對一采集或驅(qū)動，再通過電子模塊間相互通信協(xié)作完成聯(lián)鎖邏輯運算，分散了聯(lián)鎖主機的聯(lián)鎖功能。這種系

2、統(tǒng)的通信和時間參量非常重要，必須保證系統(tǒng)的安全運行。目前保證聯(lián)鎖系統(tǒng)正確性和安全性的方法有模擬、仿真和反復(fù)測試，但通過這些實驗方法對系統(tǒng)進行查錯所能涵蓋的系統(tǒng)行為有限，很難找出系統(tǒng)所有潛在的錯誤。而采用形式化方法對分散控制聯(lián)鎖系統(tǒng)行為進行建模，可以減少聯(lián)鎖系統(tǒng)設(shè)計故障，在一定程度上解決該問題。
　　 本文首先根據(jù)分散控制聯(lián)鎖系統(tǒng)功能特點和計算機聯(lián)鎖技術(shù)標(biāo)準(zhǔn)，分析設(shè)計信號電子模塊、道岔電子模塊和軌道電子模塊的進路控制工作流程，以此

3、為依據(jù)得到系統(tǒng)通信架構(gòu)和各電子模塊的具體通信過程。其次再結(jié)合時間自動機理論建立始端信號電子模塊的時間自動模型、敵對信號電子模塊的時間自動機模型、道岔電子模塊的時間自動機模型和軌道區(qū)段電子模塊的時間自動機模型。最后利用基于時間自動機理論的UPPAAL驗證工具建立系統(tǒng)進路控制過程的時間自動機網(wǎng)絡(luò)模型;使用模擬器進行隨機實驗，得到系統(tǒng)進路控制過程的仿真時序圖，分析系統(tǒng)通信過程和狀態(tài)變化;在驗證器中，用BNF語法提取系統(tǒng)待驗證的性質(zhì)，驗證分散控