通過對動態(tài)、并發(fā)和實時系統(tǒng)的形式化驗證保證其安全性已經(jīng)成為近幾十年來軟件工程研究的焦點。由Edmund M.Clarke,Allen Emerson和Joseph Sifakis等人在20世紀80年代提出的模型檢測是一種著名的軟件形式化驗證技術(shù),它主要通過顯式的系統(tǒng)狀態(tài)搜索或者隱式的不動點計算自動地驗證通信協(xié)議或者軟件系統(tǒng)的模型是否滿足要求的規(guī)格。模型檢測由于其高度自動化而在工業(yè)界備受歡迎,提出者也因此在2007年榮獲圖靈獎。但是模型檢測的狀態(tài)空間隨著系統(tǒng)組件的增加成指數(shù)增加。這個問題被稱為狀態(tài)空間爆炸問題。如何解決這個問題是當(dāng)前科學(xué)家和學(xué)者的研究熱點。在大數(shù)據(jù)和互聯(lián)網(wǎng)+的時代背景下,云計算日新月異地迅速發(fā)展。云計算通過虛擬化技術(shù)擴展計算所需的軟硬件資源,很大程度上提高了計算機的計算能力,也為應(yīng)對模型檢測的狀態(tài)空間爆炸問題提供了新的可能的解決方案。本文首先對基于時態(tài)邏輯的模型檢測技術(shù)的國內(nèi)外研究現(xiàn)狀進行了總結(jié)。然后,本文分別對云計算和大數(shù)據(jù)的起源和發(fā)展進行了深入研究,從而充分了解了云計算的發(fā)展現(xiàn)狀和應(yīng)用背景。不同的云計算的平臺通�；诓煌哪Ｐ蛯崿F(xiàn)并行分布式計算,并不能直接用于模型檢測,...

【文章頁數(shù)】：67 頁

【學(xué)位級別】：碩士

【部分圖文】：

圖1.1學(xué)者們提出的應(yīng)對模型檢測空間爆炸問題的方法

獲得了2007年的圖靈獎。但是其狀態(tài)空間的大小隨著其成指數(shù)級的增加。這個問題又被稱為狀態(tài)空間爆炸問題的狀態(tài)空間問題是當(dāng)前科學(xué)家和學(xué)者的研究熱點。者們提出的應(yīng)對模型檢測的狀態(tài)空間爆炸問題的方法如二叉判定樹是一種有效數(shù)據(jù)結(jié)構(gòu)，它可以有效表示軟件系]利用了軟件系統(tǒng)中一些交織的組件的....

圖1.2大數(shù)據(jù)平臺和云計算的關(guān)系

當(dāng)今社會是一個日新月異科技技術(shù)迅速發(fā)展的社會，人與人之間的交流、信息系統(tǒng)之間的交互越來越頻繁，大數(shù)據(jù)（bigdata）[15]就是在這樣的時代下產(chǎn)生的。對于大數(shù)據(jù)的定義，大數(shù)據(jù)的研究機構(gòu)高德納（Gartner）給出義是：大數(shù)據(jù)是需要新處理模式才能具有更強的決策力、洞察發(fā)現(xiàn)力和流....

圖2.1Kripke結(jié)構(gòu)的有向圖表示

2預(yù)備知識子公式來表示。從某種角度來看，Kripke結(jié)構(gòu)可以被看作是一機。但Kripke結(jié)構(gòu)中的節(jié)點與經(jīng)典的有限狀態(tài)自動機中的狀態(tài)是有標(biāo)記的，因此具有更加豐富的內(nèi)涵。圖2.1給出了一個K圖表示，其中可能世界集W是集合012{s,s,s}、可能世界之間二....

圖2.2資源共享協(xié)議I

進程的資源共享問題[60]是一個在計算機軟件系統(tǒng)設(shè)計過程中經(jīng)常遇到舉例來說，讀寫共享的磁盤文件或者訪問數(shù)據(jù)庫的時候都會涉及到資和互質(zhì)訪問的問題。在這類問題中，設(shè)計軟件系統(tǒng)的時候要保證共享夠被多個進程一起訪問以防出現(xiàn)不一致的問題，例如，多個進程同時個文件就必須被禁止的。因此，設(shè)計的....

本文編號：4041445