界程演算模型檢測(cè).pdf

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

2、是對(duì)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í)增加了父子界程間能夠跨界程通信的操作原語(yǔ)。SA、SAP和BA都是對(duì)MA演算的改進(jìn)，但都只是局部的

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

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

5、則對(duì)有不動(dòng)點(diǎn)算子嵌套的邏輯表達(dá)式進(jìn)行計(jì)算的全局算法的時(shí)間復(fù)雜性為O(nk+1)，其中n為變遷系統(tǒng)的狀態(tài)總數(shù)，k為不動(dòng)點(diǎn)算子嵌套深度。Long等人在分析了計(jì)算嵌套不動(dòng)點(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ì)算交替嵌套μ-演算公式的全局模型檢測(cè)算法，在目前已知的針對(duì)完全μ-演算的全局模型檢測(cè)算法中是首個(gè)空間復(fù)雜性為O(dn)且時(shí)間復(fù)雜性指數(shù)部分只有d／2的算法。算法性能的改善，使得不動(dòng)點(diǎn)算子交替嵌套深度很大的μ-演算公式的求解成為可能，這在模型檢測(cè)方面有著非常重要的意義。 3.在界程邏輯模型檢測(cè)方面。本文在林惠民院士的工作基礎(chǔ)上，討論了帶遞歸的謂詞界程邏輯在有限控制移動(dòng)界程上的模型檢測(cè)問題，首次將嵌套謂詞等式系應(yīng)用到帶遞歸的謂詞界程邏輯

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