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

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

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

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