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

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

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

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