基于模型驅(qū)動的計算機(jī)聯(lián)鎖軟件開發(fā)方法的研究與實現(xiàn).pdf

1、計算機(jī)聯(lián)鎖系統(tǒng)(CBI)是鐵路運輸中的重要設(shè)備,它肩負(fù)著列車調(diào)度、安全行車、提高運輸效率的重要工作。它通過對道岔、進(jìn)路以及信號的控制,來實現(xiàn)鐵路列車的調(diào)度指揮工作。隨著計算機(jī)技術(shù)在鐵路信號中的發(fā)展與應(yīng)用,傳統(tǒng)的分析設(shè)計方法已經(jīng)無法滿足當(dāng)前社會對于鐵路運輸?shù)陌踩?、高效性需求。為此我們采用模型?qū)動的嵌入式軟件開發(fā)方法對聯(lián)鎖軟件的設(shè)計與驗證提出了新的思路,從而提高軟件開發(fā)的精確性和高效性。
　　本文首先深入研究了各種形式化建模語言在嵌

2、入式軟件中的應(yīng)用,以及它們在當(dāng)前國際國內(nèi)的發(fā)展水平和未來發(fā)展趨勢。主要對各個方法的優(yōu)點與缺點進(jìn)行了對比分析,找出了一種適合計算機(jī)聯(lián)鎖系統(tǒng)軟件開發(fā)的以模型設(shè)計需求分析取代傳統(tǒng)文本設(shè)計需求分析的方法,即時間自動機(jī)理論。
　　本文以工大高科自主研發(fā)的計算機(jī)聯(lián)鎖系統(tǒng)軟件GKI-33e為研究對象,對它的進(jìn)路辦理流程進(jìn)行了深入的分析,根據(jù)EN系列標(biāo)準(zhǔn)以及國家鐵路標(biāo)準(zhǔn)對它的安全性和功能性進(jìn)行了主要描述,提出了軟件設(shè)計的V模型。并根據(jù)此設(shè)計流程對

3、進(jìn)路辦理流程進(jìn)行了形式化建模與分析。
　　本文針對進(jìn)路辦理中的五個主要階段分別建立了對應(yīng)的時間自動機(jī)模型,并且通過成熟的UPPAAL工具組建了時間自動機(jī)網(wǎng)絡(luò),并對該網(wǎng)絡(luò)進(jìn)行了仿真模擬,通過時間約束與全局變量的設(shè)定,解決了以往開發(fā)過程中存在的模糊性、二義性等問題。
　　最后,本文從系統(tǒng)的功能性與安全性出發(fā),對時間自動機(jī)網(wǎng)絡(luò)進(jìn)行了驗證。通過BNF語法對系統(tǒng)安全功能進(jìn)行了驗證與分析。證明了以模型驅(qū)動方法為基礎(chǔ)的嵌入式軟件開發(fā)方法的