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

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

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

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