基于eventb的聯(lián)鎖系統(tǒng)進(jìn)路控制建模與驗(yàn)證研究

《基于eventb的聯(lián)鎖系統(tǒng)進(jìn)路控制建模與驗(yàn)證研究》由會(huì)員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。

1、劣蠊交碩士學(xué)位論文基于Event．B的聯(lián)鎖系統(tǒng)進(jìn)路控制建模與驗(yàn)證研究ResearchonEvent—-BBasedModelingandVerificationofInterlockingRouteControl作者：童湖東導(dǎo)師：寧濱北京交通大學(xué)2013年3月學(xué)位論文版權(quán)使用授權(quán)擴(kuò)I墮IIIIIIIIIIIIllliiiii塑miilliiliPil吵iiiIPrJiiillilliil本學(xué)位論文作者完全了解北京交通大學(xué)有關(guān)保留、使用學(xué)位論文的規(guī)定。特授權(quán)北京交通大學(xué)可以將學(xué)位論文的全部或部分內(nèi)容編入有關(guān)數(shù)據(jù)庫進(jìn)行檢索，并采用影印、縮印或掃描等復(fù)制手段保存、匯編以供查閱和借閱。同

2、意學(xué)校向國(guó)家有關(guān)部門或機(jī)構(gòu)送交論文的復(fù)印件和磁盤。(保密的學(xué)位論文在解密后適用本授權(quán)說明)學(xué)位論文作者簽名：芻浦琢簽字日期：陽弓年夕月日中圖分類號(hào)：U284．37UDC：625學(xué)校代碼：10004密級(jí)：公開北京交通大學(xué)碩士學(xué)位論文基于Event—B的聯(lián)鎖系統(tǒng)進(jìn)路控制建模與驗(yàn)證研究ResearchonEvent—BBasedModelingandVerificationofInterlockingRouteContr01作者姓名：童湖東導(dǎo)師姓名：寧濱學(xué)位類別：工學(xué)學(xué)科專業(yè)：交通信息工程及控制學(xué)號(hào)：10120315職稱：教授學(xué)位級(jí)別：碩士研究方向：基于通信的列車運(yùn)行控制還仃弳制北京交

3、通大學(xué)2013年3月致謝本論文的工作是在我的導(dǎo)師寧濱教授的悉心指導(dǎo)下完成的，寧濱教授嚴(yán)謹(jǐn)?shù)闹螌W(xué)態(tài)度和科學(xué)的工作方法給了我極大的幫助和影響。在此衷心感謝三年來寧濱老師對(duì)我的關(guān)心和指導(dǎo)。王海峰副教授悉心指導(dǎo)我們完成了實(shí)驗(yàn)室的科研工作，在學(xué)習(xí)上和生活上都給予了我很大的關(guān)心和幫助，在此向王海峰老師表示衷心的謝意。感謝荀徑、李偉、李雷、張路、張宏韜、邊遠(yuǎn)、蔣琦、曹欣師兄和周寧、張?jiān)?、湯永、吳雅靜等同學(xué)在實(shí)驗(yàn)室工作期間給與我的熱情幫助。感謝我的父母，他們的理解和支持使我能夠在學(xué)校專心完成我的學(xué)業(yè)，在人生道路上保持前行的勇氣和動(dòng)力。中文摘要摘要：聯(lián)鎖系統(tǒng)是鐵路信號(hào)系統(tǒng)的重要組成部分，直接關(guān)系到

4、車站行車和作業(yè)的安全與效率。計(jì)算機(jī)聯(lián)鎖系統(tǒng)由于具有高效、智能化、易于維護(hù)的優(yōu)點(diǎn)而成為當(dāng)前聯(lián)鎖系統(tǒng)運(yùn)用的主流。聯(lián)鎖軟件是計(jì)算機(jī)聯(lián)鎖系統(tǒng)正確執(zhí)行聯(lián)鎖運(yùn)算、實(shí)現(xiàn)聯(lián)鎖功能的關(guān)鍵，必須具備極高的安全性和可靠性。當(dāng)前的聯(lián)鎖軟件開發(fā)主要使用傳統(tǒng)的基于軟件工程的方法，在需求定義上難以保證完備性和一致性，仿真和測(cè)試也不足以完整分析和驗(yàn)證軟件安全性，容易形成安全隱患，同時(shí)，開發(fā)出的軟件可維護(hù)性不高。本文針對(duì)傳統(tǒng)聯(lián)鎖軟件開發(fā)方法存在的問題，從實(shí)際應(yīng)用角度出發(fā)提出基于Event．B的形式化解決方案，選取聯(lián)鎖軟件核心功能——進(jìn)路控制進(jìn)行了形式化建模和驗(yàn)證的探索研究，主要研究工作如下：(1)分析了當(dāng)前聯(lián)軟件

5、開發(fā)方法存在的缺陷和引入形式化解決方案的可能性，研究了Event-B形式化建模驗(yàn)證方法的理論基礎(chǔ)和應(yīng)用特點(diǎn)，介紹了Event-B方法相關(guān)工具，提出了基于Event．B的聯(lián)鎖軟件形式化開發(fā)方法。(2)分析了聯(lián)鎖軟件進(jìn)路控制具體流程，在此基礎(chǔ)上制定了聯(lián)鎖進(jìn)路控制Event．B模型的建立步驟和精化策略，并根據(jù)制定的步驟和精化策略，在Rodin工具平臺(tái)下借助UML．B工具逐步建立了包含進(jìn)路選排、信號(hào)控制、進(jìn)路鎖閉、自動(dòng)解鎖和人工解鎖各進(jìn)程功能需求和安全需求的進(jìn)路控制Event．B模型。(3)采用模型仿真和模型證明相結(jié)合的方法對(duì)建立的聯(lián)鎖進(jìn)路控制Event．B模型進(jìn)行了形式化驗(yàn)證，其中模型

6、仿真部分采用了UML．B狀態(tài)機(jī)仿真的方法，模型證明部分則借助Event．B證明義務(wù)機(jī)制和Rodin平臺(tái)采用了自動(dòng)證明和交互式證明相結(jié)合的方法，結(jié)果表明本文所建立的進(jìn)路控制模型能覆蓋系統(tǒng)功能需求和安全需求，模型有效性、正確性和一致性能得到完整驗(yàn)證。本文的研究結(jié)果表明，基于Event．B的形式化建模驗(yàn)證方法能準(zhǔn)確和有效的描述聯(lián)鎖進(jìn)路控制的功能需求和安全需求，并且完整的分析和驗(yàn)證模型安全特性，能運(yùn)用于聯(lián)鎖軟件開發(fā)中以增強(qiáng)軟件安全性并提高開發(fā)效率。關(guān)鍵詞：聯(lián)鎖軟件；進(jìn)路控制；形式化方法；Event．B分類號(hào)：U284．37ABSTRACTABSTRACT：Asanimportantpar

7、tofrailwaysignalsystem，interlockingsystemplaysakeyroleinensuringthesafetyoftrainrunninginstationandimprovingefficiency．Computerbasedinterlockingisnowthemaindirectionofinterlockingsystemdevelopmentforitsadvantagesofhighefficiency,intelligencea