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

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

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

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