基于UML的列控系統(tǒng)建模方法與驗(yàn)證工具集成.pdf

1、近年來隨著技術(shù)的發(fā)展，列車運(yùn)行控制系統(tǒng)的功能不斷增強(qiáng)，為實(shí)現(xiàn)不同廠商設(shè)備間、地面設(shè)備與車載設(shè)備間互聯(lián)互通，使列車能夠在軌道交通網(wǎng)中跨線安全運(yùn)行，列控系統(tǒng)需求規(guī)范的作用正日益突顯。但現(xiàn)有研究成果表明在需求層面對(duì)系統(tǒng)的關(guān)鍵屬性進(jìn)行分析和確認(rèn)面臨很多困難，需要提出一種合理的框架結(jié)構(gòu)以對(duì)其關(guān)鍵屬性進(jìn)行建模并對(duì)系統(tǒng)進(jìn)行驗(yàn)證。
　　從建模方法來看，統(tǒng)一建模語言(UML)具有定義良好、易于表達(dá)、描述直觀等優(yōu)點(diǎn)，已被廣泛應(yīng)用到不同的領(lǐng)域，但當(dāng)需要

2、對(duì)影響列車安全可靠運(yùn)行的連續(xù)和離散過程進(jìn)行一體化建模時(shí)，對(duì)混成特性的描述已遠(yuǎn)遠(yuǎn)超出了這種建模語言本身的能力范圍，這給列控系統(tǒng)需求規(guī)范的建模工作帶來了巨大的挑戰(zhàn)。
　　從驗(yàn)證方法來看，形式化方法已成為保障安全苛求系統(tǒng)的安全性與可靠性的重要手段。針對(duì)不同的系統(tǒng)、同一系統(tǒng)的不同性質(zhì)和系統(tǒng)分析的不同階段，可供研究人員使用的形式化驗(yàn)證工具種類繁多。
　　因此，本文從列控系統(tǒng)需求規(guī)范建模方法與驗(yàn)證工具集成著手進(jìn)行研究，主要內(nèi)容包括：

3、r>　　1.對(duì)列控系統(tǒng)需求規(guī)范混成特性建模需求進(jìn)行分析，研究UML擴(kuò)展機(jī)制，充分挖掘UML的圖形功能，設(shè)計(jì)面向列控系統(tǒng)需求規(guī)范的混成UML概要文件，使之能夠包含更多的內(nèi)容與信息去準(zhǔn)確地刻畫列控系統(tǒng)的混成特性。
　　2.在論述列控系統(tǒng)需求規(guī)范的分析方法體系結(jié)構(gòu)的基礎(chǔ)上，重點(diǎn)分析了模型驗(yàn)證階段的功能需求。在Eclipse平臺(tái)上完成了驗(yàn)證支持工具的軟件原型開發(fā)，對(duì)底層形式化建模過程和驗(yàn)證工具進(jìn)行封裝，通過自動(dòng)化的模型檢驗(yàn)技術(shù)來尋找需求中

4、隱藏的錯(cuò)誤，使現(xiàn)有的需求管理工具(IBM RequisitePro)、建模工具(IBMRational Software Architect)和驗(yàn)證工具(NuSMV，PHAVer)實(shí)現(xiàn)高度集成，并具備良好的可擴(kuò)展性。并給出從UML模型到形式化模型的轉(zhuǎn)換規(guī)則，構(gòu)造了面向?qū)ο笳Z言UML以及NuSMV、PHAVer形式化語言之間的轉(zhuǎn)換橋梁。
　　3.從列控系統(tǒng)需求規(guī)范中選取了具有代表性的模式轉(zhuǎn)換場(chǎng)景和RBC交接場(chǎng)景，利用所提出的混成UM