界程演算模型檢測.pdf

1、本文的研究工作主要有以下幾個方面； 1. 在界程演算方面。由于在移動界程(Mobile Ambients，MA)中，in、out、open操作可以不受限進行，環(huán)境對自身邊界沒有任何管理權限，并且由于MA中open操作的存在，兩個原本不在一塊的進程能通過open操作后處在同一環(huán)境中，這樣可導致兩個進程間意想不到的交互(干擾)的產(chǎn)生。為了克服這些不足，安全環(huán)境演算(Safe Ambients，SA)中增加了in、out、open協(xié)操作，分別

2、是對in、out、open操作的許可；帶口令的安全界程演算(Safe Ambients with Password，SAP)SAP在in、out，open、in、out、open操作中增加口令(或通道>，只有掌握口令(或通道)的進程才能進行in、out、open操作；盒子界程演算(Boxed Ambients，BA)中取消了open操作，同時增加了父子界程間能夠跨界程通信的操作原語。SA、SAP和BA都是對MA演算的改進，但都只是局部的

3、改進，最終SA、SAP不能避免由于open操作帶來的干擾，BA也控制不了in和out操作對界程邊界的隨意穿越。同時由于BA中無open操作，界程一旦建立，將永遠停留在系統(tǒng)中，這樣將占用大量的系統(tǒng)資源，也不符合進程的實際情況。為了克服MA、SA、SAP和BA的不足，本文提出了一個帶口令的安全盒子界程演算(Safe Boxed Ambients with Password，SBAP)。相對于MA，BSAP做了如下幾點改進；(1)取消了MA中

4、的open操作，增加了父子界程間的通信操作原語；(2)增加了in、out操作，并在in、out、in、out操作中加入了密碼；(3)增加了界程回收操作原語del。通過用SBAP對Internet上的電子郵件系統(tǒng)進行描述和仿真以及對進程死鎖的實時處理，說明SBAP在網(wǎng)絡計算方面有一定的表現(xiàn)能力。 2.在mu-演算模型檢測方面。針對完全μ-演算的全局模型檢測算法的設計，根據(jù)Tarski's不動點定理，公式中的不動點算子直接用逐次迭代來計算，

5、則對有不動點算子嵌套的邏輯表達式進行計算的全局算法的時間復雜性為O(nk+1)，其中n為變遷系統(tǒng)的狀態(tài)總數(shù)，k為不動點算子嵌套深度。Long等人在分析了計算嵌套不動點表達式的中間結果間的偏序關系找到了一個時間復雜性為O(n[d/2]+1)，空間復雜性為指數(shù)的全局計算算法。本文在Long等人工作的基礎上，根據(jù)μ-演算公式中函數(shù)的單調特性，提出了一個時間復雜性為O((2n+1)[(d+3)/4]+[(d+2)/4])，空間復雜性為O(dn)

6、的計算交替嵌套μ-演算公式的全局模型檢測算法，在目前已知的針對完全μ-演算的全局模型檢測算法中是首個空間復雜性為O(dn)且時間復雜性指數(shù)部分只有d／2的算法。算法性能的改善，使得不動點算子交替嵌套深度很大的μ-演算公式的求解成為可能，這在模型檢測方面有著非常重要的意義。 3.在界程邏輯模型檢測方面。本文在林惠民院士的工作基礎上，討論了帶遞歸的謂詞界程邏輯在有限控制移動界程上的模型檢測問題，首次將嵌套謂詞等式系應用到帶遞歸的謂詞界程邏輯

7、模型檢測中，提出了一個時間復雜性與邏輯公式的交錯嵌套深度呈指數(shù)關系的局部模型檢測算法，這是目前首個有明確時間復雜性的謂詞界程邏輯模型檢測算法，也是目前已知的第二個帶遞歸的謂詞界程邏輯模型檢測算法。所做的工作主要有：(1)討論了謂詞界程邏輯公式與嵌套謂詞等式系間語義的等價性，給出了謂訶界程邏輯公式轉換成嵌套謂詞等式系的方法；(2)討論了不動點算子無交錯的謂詞界程邏輯模型檢測問題，給出了具體算法；(3)討論了不動點算子交錯嵌套情況下的謂詞界