形式驗證及其在網(wǎng)格計算環(huán)境中的應(yīng)用.pdf

1、形式驗證是一種比測試和模擬更具吸引力的描述和驗證軟硬件系統(tǒng)的方法.形式驗證方法的種類很多,從定理證明到計算機輔助定理證明,最后出現(xiàn)模型檢測方法.該文所提出的兩個緩解狀態(tài)爆炸現(xiàn)象的方法都是在現(xiàn)有方法的基礎(chǔ)上加以改進或拓寬適用范圍.其一,在最近由Glenn提出的部分狀態(tài)空間模型檢測技術(shù)的基礎(chǔ)上,討論一類具有公平性約束條件的CTL(計算樹邏輯)模型檢測問題.部分狀態(tài)空間模型檢測方法只搜索部分狀態(tài)空間,通過定義一個序關(guān)系來表達部分狀態(tài)空間之間的

2、關(guān)系.其二,鑒于目前所提出的分布式模型檢測算法破壞了原有順序算法的嵌套深度優(yōu)先搜索順序,因此不能驗證LTL公式.我們提出了一種能夠保持深度優(yōu)先搜索序的分布式嵌套深度優(yōu)先算法(DDDFA)來驗證LTL公式所刻畫的屬性.論文還討論了網(wǎng)格計算環(huán)境下信息服務(wù)體系結(jié)構(gòu),為了實現(xiàn)網(wǎng)格計算環(huán)境中大規(guī)模資源共享的目標,需要定義一個靈活、安全、協(xié)調(diào)的資源共享機制,這種共享機制是建立在某個通過動態(tài)組合個體、機構(gòu)及資源而構(gòu)成的VO上的.而VO范例的實現(xiàn)依賴于

3、分布式目錄服務(wù),即目錄服務(wù)趨于分布.但分布的一個后果就是它很難提供給用戶一個準確的信息,因此分布式目錄服務(wù)的主要任務(wù)就集中到如何準確獲得一個實體的位置信息.該文工作的最主要的意義是:鑒于現(xiàn)有驗證無限狀態(tài)系統(tǒng)(特指參數(shù)化系統(tǒng))的方法,幾乎都是從系統(tǒng)的符號化模型開始進行到達性分析,該文定義了一個可以直觀描述參數(shù)化系統(tǒng)的語言PSL,并給出直接從PSL腳本自動生成符合化模型的算法.因此,我們的工作是最新的,它使驗證參數(shù)化系統(tǒng)更自動更完整.另外,