面向環(huán)境演算系統(tǒng)的模型檢測(cè)算法的研究.pdf

1、作為一種很重要的自動(dòng)驗(yàn)證技術(shù)，模型檢測(cè)已得到廣泛研究，取得了豐碩的成果并應(yīng)用到眾多領(lǐng)域，引起學(xué)術(shù)界、工業(yè)界的密切關(guān)注。
　　 模型檢測(cè)的一般原理是用狀態(tài)遷移系統(tǒng)(M)表示系統(tǒng)的行為，用模態(tài)邏輯公式(φ)描述系統(tǒng)的屬性。這樣“系統(tǒng)是否具有所期望的性質(zhì)?”就轉(zhuǎn)化為數(shù)學(xué)問(wèn)題“狀態(tài)遷移系統(tǒng)M是否是公式φ的一個(gè)模型?”。
　　 因此，模型檢測(cè)的研究主要圍繞在為待測(cè)系統(tǒng)建模和采用某種方法正確有效地刻畫待測(cè)系統(tǒng)的屬性這兩個(gè)方面進(jìn)行。本

2、文研究的系統(tǒng)主要是用于對(duì)廣域網(wǎng)和因特網(wǎng)上的計(jì)算模型建模的環(huán)境演算系統(tǒng)，刻畫該系統(tǒng)的屬性采用的是模態(tài)邏輯中的空間邏輯并結(jié)合時(shí)態(tài)邏輯，分別從進(jìn)程的結(jié)構(gòu)性質(zhì)與歸約動(dòng)作兩方面進(jìn)行描述。本文所做的主要工作如下：
　　 (1)首先研究了環(huán)境演算系統(tǒng)中的移動(dòng)環(huán)境演算、安全環(huán)境演算和盒子環(huán)境演算，在已有的相關(guān)研究的基礎(chǔ)上對(duì)這三個(gè)系統(tǒng)進(jìn)行縱向的分析與比較，并分別給出了系統(tǒng)模擬與示例。
　　 (2)基于對(duì)上述三個(gè)環(huán)境演算的分析，給出了它們對(duì)

3、應(yīng)的面向歸約語(yǔ)義的空間邏輯。一方面，該邏輯的靜態(tài)部分刻畫進(jìn)程的結(jié)構(gòu)，這部分不僅包含了傳統(tǒng)的結(jié)構(gòu)算子，而且還引入了新的描述進(jìn)程前綴動(dòng)作的邏輯算子。另一方面，該邏輯的動(dòng)態(tài)部分刻畫進(jìn)程的歸約動(dòng)作，即做一步τ-動(dòng)作后進(jìn)程滿足某些性質(zhì)，本文不采用進(jìn)程的行為動(dòng)作語(yǔ)義，因此邏輯中不必考慮in、out等動(dòng)作執(zhí)行的情況。
　　 (3)分別為本文研究的模型系統(tǒng)和邏輯系統(tǒng)給出了相應(yīng)的數(shù)據(jù)結(jié)構(gòu)表示，并基于模型檢測(cè)技術(shù)的原理來(lái)判斷模型系統(tǒng)是否具有對(duì)應(yīng)邏輯