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