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

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

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

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