列控系統(tǒng)混成行為的建模與驗(yàn)證方法.pdf

1、隨著列控技術(shù)的發(fā)展，列車運(yùn)行控制系統(tǒng)獲得了巨大的進(jìn)步和發(fā)展。在系統(tǒng)的設(shè)計(jì)和開發(fā)階段，為了確保列控系統(tǒng)的安全性，列控系統(tǒng)需求規(guī)范的正確性起著越來(lái)越重要的作用。然而，在系統(tǒng)開發(fā)的初始階段，通常會(huì)因?yàn)橄到y(tǒng)需求規(guī)范不完整而無(wú)法進(jìn)行開發(fā)。在這種情況下，如何確定系統(tǒng)的關(guān)鍵參數(shù)成為主要的研究課題。同時(shí)，現(xiàn)有研究成果表明，在需求層面，分析和驗(yàn)證系統(tǒng)模型中的關(guān)鍵參數(shù)面臨很多困難。因此，為了解決系統(tǒng)模型中關(guān)鍵參數(shù)的分析問(wèn)題，需要提出一種合理的系統(tǒng)屬性建模和

2、形式化驗(yàn)證的框架結(jié)構(gòu)。
　　列控系統(tǒng)需求規(guī)范的分析過(guò)程包括兩部的內(nèi)容，建立系統(tǒng)規(guī)范模型和對(duì)該形式化模型進(jìn)行驗(yàn)證。一方面，統(tǒng)一建模語(yǔ)言(UML)是一種面向?qū)ο蟮慕ＵZ(yǔ)言，已廣泛應(yīng)用于不同工程領(lǐng)域。然而，列控系統(tǒng)屬于典型的混成系統(tǒng)和安全苛求系統(tǒng)。正確地刻畫系統(tǒng)的混成特性給列控系統(tǒng)需求規(guī)范的建模工作帶來(lái)了巨大的挑戰(zhàn)。另一方面，形式化方法已成為保障安全苛求系統(tǒng)的安全性與可靠性的重要手段。根據(jù)不同的分析或驗(yàn)證要求，設(shè)計(jì)者可以選擇不同的形式化

3、驗(yàn)證工具進(jìn)行相關(guān)的驗(yàn)證工作。
　　因此，本文從列控系統(tǒng)需求規(guī)范建模方法與驗(yàn)證工具集成著手進(jìn)行研究，主要內(nèi)容包括:
　　1.對(duì)列控系統(tǒng)混成特性進(jìn)行分析，研究UML擴(kuò)展機(jī)制，設(shè)計(jì)混成UML概要文件，使之能夠準(zhǔn)確地刻畫列控系統(tǒng)的混成特性。
　　2.為了驗(yàn)證混成系統(tǒng)的安全性，提出了時(shí)間有界的可達(dá)性分析算法。該算法基于BMC驗(yàn)證技術(shù)，對(duì)具體的自動(dòng)機(jī)模型運(yùn)用該算法可以計(jì)算有界時(shí)間內(nèi)系統(tǒng)的所有可執(zhí)行路徑。時(shí)間有界的可達(dá)性分析算法適用

4、于線性或非線性混成自動(dòng)機(jī)的驗(yàn)證。
　　3.以移動(dòng)閉塞中的追蹤模型為案例，運(yùn)用提出的混成UML概要文件對(duì)其進(jìn)行建模;并根據(jù)轉(zhuǎn)換規(guī)則將所建的列車追蹤擴(kuò)展模型轉(zhuǎn)換為HYTECH模型;在開發(fā)的驗(yàn)證支持工具中完成了該模型的驗(yàn)證分析工作。通過(guò)案例分析，證明所提出的基于UML擴(kuò)展機(jī)制對(duì)列控系統(tǒng)混成行為建模方法的可行性，以及所開發(fā)驗(yàn)證支持工具的可用性。
　　4.在Topcased平臺(tái)上完成了驗(yàn)證工具的軟件開發(fā)。Topcased平臺(tái)上集成了U