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

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

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

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