界程演算模型檢測.pdf

1、本文的研究工作主要有以下幾個(gè)方面； 1. 在界程演算方面。由于在移動界程(Mobile Ambients，MA)中，in、out、open操作可以不受限進(jìn)行，環(huán)境對自身邊界沒有任何管理權(quán)限，并且由于MA中open操作的存在，兩個(gè)原本不在一塊的進(jìn)程能通過open操作后處在同一環(huán)境中，這樣可導(dǎo)致兩個(gè)進(jì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操作中增加口令(或通道>，只有掌握口令(或通道)的進(jìn)程才能進(jìn)行in、out、open操作；盒子界程演算(Boxed Ambients，BA)中取消了open操作，同時(shí)增加了父子界程間能夠跨界程通信的操作原語。SA、SAP和BA都是對MA演算的改進(jìn)，但都只是局部的

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

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

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

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

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