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

《基于uml的列控系統(tǒng)建模方法與驗(yàn)證工具集成》由會(huì)員上傳分享，免費(fèi)在線(xiàn)閱讀，更多相關(guān)內(nèi)容在行業(yè)資料-天天文庫(kù)。

1、致謝首先我要衷心地感謝我的導(dǎo)師唐濤教授對(duì)我論文的指導(dǎo)。兩年來(lái)，教授嚴(yán)謹(jǐn)?shù)闹螌W(xué)態(tài)度、精益求精的工作態(tài)度和平易近人的學(xué)者風(fēng)范，使我受益匪戰(zhàn)：教授的悉心指導(dǎo)給我極大的幫助和影響。在此，謹(jǐn)向唐老師致以衷心的感謝和崇高的敬意!特別感謝實(shí)驗(yàn)室的趙林老師。趙老師悉一15,指導(dǎo)我的科研和論文，每當(dāng)我拿著問(wèn)題去請(qǐng)教他時(shí)，他總是立刻放下手頭的工作，認(rèn)真細(xì)致的為我解惑答疑，使我學(xué)習(xí)了很多知識(shí)．提高了自己的能力，在此表示衷心的感謝。感謝實(shí)驗(yàn)室的徐田華、鄭偉等老師．這些老師在科研工作中為我提出了許多寶貴的意見(jiàn)，您們給予我的幫助，我將終生銘記。此外，我還要感謝我的師

2、兄謝雨飛、劉金濤、i4超、柴銘、劉玉鵬師兄和唐武梅、曹妍師蛆，還有同學(xué)李水康、魯秋子、林虹、周寧以及其他師弟師妹們。借此機(jī)會(huì)，我還要感謝培養(yǎng)我長(zhǎng)大含辛茹苦的父母，你們的理解和支持使我能夠在學(xué)校專(zhuān)心完成學(xué)業(yè)。謝謝你們!本論文由國(guó)家科技部863項(xiàng)目“軌道交通CPS系統(tǒng)∞感知、運(yùn)行和安全技術(shù)應(yīng)用驗(yàn)證”(項(xiàng)目編弓：201IAA010104)支持。北京交通大學(xué)碩士學(xué)位論文中文摘要摘要；近年來(lái)隨著技術(shù)的發(fā)展，列車(chē)運(yùn)行控制系統(tǒng)的功能不斷增強(qiáng)，為實(shí)現(xiàn)不同廠(chǎng)商設(shè)備問(wèn)、地面設(shè)備與車(chē)載設(shè)備問(wèn)互聯(lián)互通，使列車(chē)能夠在軌道交通網(wǎng)中跨線(xiàn)安全運(yùn)行，列控系統(tǒng)需求規(guī)范的作用

3、正日益突顯。但現(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)證。從速模方法來(lái)看．統(tǒng)一建模語(yǔ)言(uML)具有定義良好、易于表達(dá)、描述直觀(guān)等優(yōu)點(diǎn)，已被廣泛應(yīng)用到不同的領(lǐng)域．但當(dāng)需要對(duì)影響列車(chē)安全可靠運(yùn)行的連續(xù)和離散過(guò)程進(jìn)行～體化建模時(shí)，對(duì)混成特性的描述己遠(yuǎn)遠(yuǎn)超出了這種建模語(yǔ)言本身的能力范圍，這給列控系統(tǒng)需求規(guī)范的建模工作帶來(lái)了巨大的挑戰(zhàn)。從驗(yàn)證方法來(lái)看．形式化方法己成為保障安全苛求系統(tǒng)的安全性與可靠性的重要手段。針對(duì)不同的系統(tǒng)、同一系統(tǒng)的不同性質(zhì)和系統(tǒng)分析的

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

5、中脖藏的錯(cuò)誤，使現(xiàn)有的需求管理工具(IBMRequisitePro)、建摸工具fIBMRationalSottwareArchited、和驗(yàn)證1具(NuSMV，PHAVer)實(shí)現(xiàn)高度集成，并具備良好的可擴(kuò)展性。并給出MUML模型到形式化模型的轉(zhuǎn)換規(guī)則．構(gòu)造了面向?qū)ο笳Z(yǔ)言UML以及NuSMV、PHAVer形式化語(yǔ)言之間的轉(zhuǎn)換橋梁。3從列控系統(tǒng)需求規(guī)范中選取了具有代表性的模式轉(zhuǎn)換場(chǎng)景和RBC交接場(chǎng)景，利用所提出的混成UML概要文件對(duì)場(chǎng)景進(jìn)行建模；將建好的模式轉(zhuǎn)換場(chǎng)景模型轉(zhuǎn)換為NuSMV模型，而將RBC交接場(chǎng)景模型轉(zhuǎn)換為PHAVcr模型；在開(kāi)發(fā)

6、的驗(yàn)證支持工具中完成兩個(gè)形式化模型的驗(yàn)證分析工作。通過(guò)案例分析，證明文中所提出的基于UML擴(kuò)展機(jī)制的列控系統(tǒng)需求規(guī)范建模方法的可行性．以及所開(kāi)技驗(yàn)證支持工具的可用性。關(guān)鍵詞：列控秉統(tǒng)；需求規(guī)范：UML概要文件；驗(yàn)證支持工具：PHAVer；NuSMV分類(lèi)號(hào)．u2：：墊室奎塑查堂翌主蘭堡墮蘭!奎些墨北京交通大學(xué)碩士學(xué)位論文ABSTRACTABSTRACT：Withthedevelopmentofscienceandtechnology，TrainControlSystem’functionshavedevelopedintoanewstage

7、Inordertorealizetheconnectionbetweendifferentequipmentsproducedbydifferentmanufactures，andtoinsurethesafetyoftheTrainControlSystematthesametime，TrainControlSystem’sSystemRequirementSpecification(SRS)hasplayedamoreandmoreimpertsntroleinresearchanddevelopmentHowever，current

8、studiesshowthatthereexistalotofdifficultiesfortheanalysisandvalidationworkofthecriticalpropertie