鐵路信號聯(lián)鎖系統(tǒng)安全規(guī)范的形式化描述與驗證方法.pdf

1、鐵路信號的根本功能是保障列車運行安全、提高運輸效率，車站聯(lián)鎖系統(tǒng)是鐵路信號的核心技術(shù)裝備，它通過對信號機、道岔和進(jìn)路的控制來指揮行車、防止列車沖突。隨著計算機聯(lián)鎖系統(tǒng)的應(yīng)用推廣，聯(lián)鎖系統(tǒng)對軟件的依賴性越來越強，如何提高聯(lián)鎖軟件的質(zhì)量、確保系統(tǒng)安全是近年來軌道交通領(lǐng)域研究的熱點問題。聯(lián)鎖系統(tǒng)安全規(guī)范的嚴(yán)格描述與驗證對保障軟件開發(fā)質(zhì)量具有重要意義。
　　本文從我國鐵路信號聯(lián)鎖邏輯控制電路入手，深入分析提煉聯(lián)鎖系統(tǒng)的安全規(guī)范，利用形式化

2、方法進(jìn)行嚴(yán)格的描述與分析驗證，具體工作如下:
　　1.查閱大量文獻(xiàn)，論文首先對形式化方法在鐵路領(lǐng)域的應(yīng)用進(jìn)行了深入的分析和綜述，闡述了聯(lián)鎖系統(tǒng)開發(fā)過程存在的規(guī)范表達(dá)二義性和不精確問題;
　　2.結(jié)合形式化方法的發(fā)展趨勢，研究了普適性形式化規(guī)格描述與驗證方法，并對當(dāng)前流行的方法進(jìn)行了分類總結(jié)，深入探討了Event-B方法。
　　3.深入研究了6502電氣集中聯(lián)鎖邏輯控制電路，結(jié)合站場圖，重點分析了信號開放控制、四線制道岔

3、控制電路、進(jìn)路建立和分段解鎖等聯(lián)鎖關(guān)鍵環(huán)節(jié)，提煉出關(guān)鍵環(huán)節(jié)的聯(lián)鎖系統(tǒng)的安全規(guī)范。利用邏輯語義和一階謂詞邏輯對安全規(guī)范進(jìn)行了形式化描述。
　　4.結(jié)合具體的站場實例，基于Event-B方法，利用Rodin平臺，對信號開放、道岔控制、進(jìn)路解鎖等聯(lián)鎖系統(tǒng)關(guān)鍵安全規(guī)范進(jìn)行了形式化模型描述和驗證分析，給出了嚴(yán)格的分析結(jié)果。
　　工作表明，鐵路信號聯(lián)鎖系統(tǒng)是具有復(fù)雜時序邏輯的控制系統(tǒng)，Event-B方法適合于該類系統(tǒng)的描述與驗證。通過形