基于云計(jì)算平臺(tái)的時(shí)態(tài)邏輯模型檢測(cè)算法研究與實(shí)現(xiàn).pdf

1、通過(guò)對(duì)動(dòng)態(tài)、并發(fā)和實(shí)時(shí)系統(tǒng)的形式化驗(yàn)證保證其安全性已經(jīng)成為近幾十年來(lái)軟件工程研究的焦點(diǎn)。由Edmund M. Clarke，Allen Emerson和Joseph Sifakis等人在20世紀(jì)80年代提出的模型檢測(cè)是一種著名的軟件形式化驗(yàn)證技術(shù)，它主要通過(guò)顯式的系統(tǒng)狀態(tài)搜索或者隱式的不動(dòng)點(diǎn)計(jì)算自動(dòng)地驗(yàn)證通信協(xié)議或者軟件系統(tǒng)的模型是否滿足要求的規(guī)格。模型檢測(cè)由于其高度自動(dòng)化而在工業(yè)界備受歡迎，提出者也因此在2007年榮獲圖靈獎(jiǎng)。但是模型

2、檢測(cè)的狀態(tài)空間隨著系統(tǒng)組件的增加成指數(shù)增加。這個(gè)問(wèn)題被稱為狀態(tài)空間爆炸問(wèn)題。如何解決這個(gè)問(wèn)題是當(dāng)前科學(xué)家和學(xué)者的研究熱點(diǎn)。在大數(shù)據(jù)和互聯(lián)網(wǎng)+的時(shí)代背景下，云計(jì)算日新月異地迅速發(fā)展。云計(jì)算通過(guò)虛擬化技術(shù)擴(kuò)展計(jì)算所需的軟硬件資源，很大程度上提高了計(jì)算機(jī)的計(jì)算能力，也為應(yīng)對(duì)模型檢測(cè)的狀態(tài)空間爆炸問(wèn)題提供了新的可能的解決方案。
　　本文首先對(duì)基于時(shí)態(tài)邏輯的模型檢測(cè)技術(shù)的國(guó)內(nèi)外研究現(xiàn)狀進(jìn)行了總結(jié)。然后，本文分別對(duì)云計(jì)算和大數(shù)據(jù)的起源和發(fā)展進(jìn)

3、行了深入研究，從而充分了解了云計(jì)算的發(fā)展現(xiàn)狀和應(yīng)用背景。不同的云計(jì)算的平臺(tái)通?；诓煌哪Ｐ蛯?shí)現(xiàn)并行分布式計(jì)算，并不能直接用于模型檢測(cè)，并且通常還需要重新分析相應(yīng)的問(wèn)題。這是本文要研究和解決的問(wèn)題。目前基于云計(jì)算平臺(tái)的模型檢測(cè)方法主要應(yīng)用實(shí)現(xiàn)了并行計(jì)算模型MapReduce的云計(jì)算平臺(tái)Hadoop。然而，Hadoop被設(shè)計(jì)用來(lái)解決大數(shù)據(jù)的批處理問(wèn)題，對(duì)迭代計(jì)算支持的欠佳。而時(shí)態(tài)邏輯模型檢測(cè)方法可以歸約為圖計(jì)算，在計(jì)算的過(guò)程中通常存在多次