資源描述：
《基于云計(jì)算平臺(tái)的時(shí)態(tài)邏輯模型檢測(cè)算法研究與實(shí)現(xiàn)》由會(huì)員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。
1、學(xué)校代碼10459學(xué)號(hào)或申請(qǐng)?zhí)?01312172060密級(jí)碩士學(xué)位論文基于云計(jì)算平臺(tái)的時(shí)態(tài)邏輯模型檢測(cè)算法研究與實(shí)現(xiàn)作者姓名：段廷銀導(dǎo)師姓名：周清雷學(xué)科門類：工科專業(yè)名稱：軟件工程培養(yǎng)院系：信息工程學(xué)院完成時(shí)間：2016年5月AthesissubmittedtoZhengzhouUniversityforthedegreeofMasterResearchandImplementationofTemporalLogicModelCheckingAlgorithmbasedonCloudComputingPlatformByTin
2、gyinDuanSupervisor:Prof.QingLeiZhouSoftwareEngineeringSchoolofInformationEngineeringMay,2016學(xué)位論文原創(chuàng)性聲明本人鄭重聲明：所呈交的學(xué)位論文，是本人在導(dǎo)師的指導(dǎo)下，獨(dú)立進(jìn)行研究所取得的成果。除文中已經(jīng)標(biāo)注引用的內(nèi)容外，本論文不包含任何其他個(gè)人或集體已經(jīng)發(fā)表或撰寫過的科研成果。對(duì)本文的研究作出重要貢獻(xiàn)的個(gè)人和集體，均已在文中以明確方式標(biāo)明。本聲明的法律責(zé)任由本人承擔(dān)。學(xué)位論文作者：日期：年月日學(xué)位論文使用授權(quán)聲明本人在導(dǎo)師指導(dǎo)下完成的論文
3、及相關(guān)的職務(wù)作品，知識(shí)產(chǎn)權(quán)歸屬鄭州大學(xué)。根據(jù)鄭州大學(xué)有關(guān)保留、使用學(xué)位論文的規(guī)定，同意學(xué)校保留或向國家有關(guān)部門或機(jī)構(gòu)送交論文的復(fù)印件和電子版，允許論文被查閱和借閱；本人授權(quán)鄭州大學(xué)可以將本學(xué)位論文的全部或部分編入有關(guān)數(shù)據(jù)庫進(jìn)行檢索，可以采用影印、縮印或者其他復(fù)制手段保存論文和匯編本學(xué)位論文。本人離校后發(fā)表、使用學(xué)位論文或與該學(xué)位論文直接相關(guān)的學(xué)術(shù)論文或成果時(shí)，第一署名單位仍然為鄭州大學(xué)。保密論文在解密后應(yīng)遵守此規(guī)定。學(xué)位論文作者：日期：年月日摘要摘要通過對(duì)動(dòng)態(tài)、并發(fā)和實(shí)時(shí)系統(tǒng)的形式化驗(yàn)證保證其安全性已經(jīng)成為近幾十年來軟件工程研
4、究的焦點(diǎn)。由EdmundM.Clarke，AllenEmerson和JosephSifakis等人在20世紀(jì)80年代提出的模型檢測(cè)是一種著名的軟件形式化驗(yàn)證技術(shù)，它主要通過顯式的系統(tǒng)狀態(tài)搜索或者隱式的不動(dòng)點(diǎn)計(jì)算自動(dòng)地驗(yàn)證通信協(xié)議或者軟件系統(tǒng)的模型是否滿足要求的規(guī)格。模型檢測(cè)由于其高度自動(dòng)化而在工業(yè)界備受歡迎，提出者也因此在2007年榮獲圖靈獎(jiǎng)。但是模型檢測(cè)的狀態(tài)空間隨著系統(tǒng)組件的增加成指數(shù)增加。這個(gè)問題被稱為狀態(tài)空間爆炸問題。如何解決這個(gè)問題是當(dāng)前科學(xué)家和學(xué)者的研究熱點(diǎn)。在大數(shù)據(jù)和互聯(lián)網(wǎng)+的時(shí)代背景下，云計(jì)算日新月異地迅速發(fā)展
5、。云計(jì)算通過虛擬化技術(shù)擴(kuò)展計(jì)算所需的軟硬件資源，很大程度上提高了計(jì)算機(jī)的計(jì)算能力，也為應(yīng)對(duì)模型檢測(cè)的狀態(tài)空間爆炸問題提供了新的可能的解決方案。本文首先對(duì)基于時(shí)態(tài)邏輯的模型檢測(cè)技術(shù)的國內(nèi)外研究現(xiàn)狀進(jìn)行了總結(jié)。然后，本文分別對(duì)云計(jì)算和大數(shù)據(jù)的起源和發(fā)展進(jìn)行了深入研究，從而充分了解了云計(jì)算的發(fā)展現(xiàn)狀和應(yīng)用背景。不同的云計(jì)算的平臺(tái)通?；诓煌哪Ｐ蛯?shí)現(xiàn)并行分布式計(jì)算，并不能直接用于模型檢測(cè)，并且通常還需要重新分析相應(yīng)的問題。這是本文要研究和解決的問題。目前基于云計(jì)算平臺(tái)的模型檢測(cè)方法主要應(yīng)用實(shí)現(xiàn)了并行計(jì)算模型MapReduce的云計(jì)算
6、平臺(tái)Hadoop。然而，Hadoop被設(shè)計(jì)用來解決大數(shù)據(jù)的批處理問題，對(duì)迭代計(jì)算支持的欠佳。而時(shí)態(tài)邏輯模型檢測(cè)方法可以歸約為圖計(jì)算，在計(jì)算的過程中通常存在多次迭代，基于Hadoop的模型檢測(cè)方法往往具有較高的延遲。針對(duì)以上問題，本文提出了基于BSP消息傳遞模型的時(shí)態(tài)邏輯模型檢測(cè)方法，設(shè)計(jì)了基于云計(jì)算平臺(tái)Giraph的模型檢測(cè)器的系統(tǒng)模型并實(shí)現(xiàn)了其偽分布式模式。在相同硬件情況下的對(duì)照實(shí)驗(yàn)表明本文提出的方法很大程度上優(yōu)于基于Hadoop的方法。這是本文的主要?jiǎng)?chuàng)新點(diǎn)。上述所做的工作，進(jìn)一步完善了基于云計(jì)算平臺(tái)的模型檢測(cè)理論體系和技術(shù)
7、范疇。關(guān)鍵字：時(shí)態(tài)邏輯模型檢測(cè)云計(jì)算HadoopGirpahMapReduceBSPIAbstractAbstractToensurethesecuritybyformalverificationofdynamic,concurrentandreal-timesystemshasbeenthefocusofsoftwareengineeringresearchforseveraldecades.ModelcheckingproposedbyEdmundM.Clark,AllenEmersonandJosephSifakisin
8、theeightiesofthe20thcenturyisadistinguishedformalverificationtechnology,whichautomaticallyverifieswhetherthecommunicationprotocolorthesyst
