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

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

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

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