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

1、通過對動態(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年榮獲圖靈獎。但是模型

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

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