【摘要】： 近10年來(lái),以界程演算(Mobile Ambients)為代表移動(dòng)進(jìn)程演算模型已成為移動(dòng)計(jì)算形式化理論的研究熱點(diǎn),但相對(duì)于理論研究方面的豐富成果,模型實(shí)用化方面研究相對(duì)較少,特別是將界程演算實(shí)際應(yīng)用于移動(dòng)計(jì)算系統(tǒng)的核心程序語(yǔ)言,或系統(tǒng)建模語(yǔ)言的應(yīng)用界程演算模型,以及相關(guān)模型檢測(cè)系統(tǒng)的實(shí)現(xiàn)等方面還有待進(jìn)一步研究。本文針對(duì)上述問(wèn)題,在面向移動(dòng)計(jì)算系統(tǒng)建模應(yīng)用的擴(kuò)展界程演算、界程演算的空間邏輯、偏序模型檢測(cè)方法以及模型檢測(cè)系統(tǒng)實(shí)現(xiàn)框架等方面進(jìn)行了研究。主要工作包括: 1、提出了以“界程”為核心概念的、面向移動(dòng)計(jì)算系統(tǒng)建模應(yīng)用的擴(kuò)展演算模型。本文針對(duì)移動(dòng)計(jì)算系統(tǒng)的建模語(yǔ)言需要表達(dá)IF-THEN-ELSE語(yǔ)義以及模型性質(zhì)的自動(dòng)驗(yàn)證需要系統(tǒng)模型保持有限狀態(tài)性質(zhì)這一命題進(jìn)行了研究,提出了一種擴(kuò)展界程演算模型--應(yīng)用界程演算(簡(jiǎn)稱Applied-AC演算)。該演算首先在現(xiàn)有界程擴(kuò)展演算中引入IF-THEN-ELSE結(jié)構(gòu)的進(jìn)程,并采用帶參數(shù)的遞歸進(jìn)程結(jié)構(gòu)來(lái)表示進(jìn)程的重復(fù)執(zhí)行。該演算引入一種標(biāo)準(zhǔn)化操作來(lái)處理IF-THEN-ELSE結(jié)構(gòu)進(jìn)程的語(yǔ)義,簡(jiǎn)化了模型檢測(cè)時(shí)空間邏輯語(yǔ)義的復(fù)雜性。該演算還研究了Applied-AC演算的有限控制進(jìn)程的問(wèn)題,采用類型系統(tǒng)來(lái)保證Applied-AC進(jìn)程在基于結(jié)構(gòu)同余所確立的等價(jià)關(guān)系下的有限控制性,并研究了有限控制的Applied-AC演算對(duì)有限PI演算進(jìn)程的翻譯方法。本文采用的類型系統(tǒng)和有限控制界程演算對(duì)有限PI演算的翻譯方法可推廣應(yīng)到到其它所有含有協(xié)動(dòng)作原語(yǔ)的界程演算擴(kuò)展模型。 2、提出了一種可判定的、融合了空間模態(tài)和行為模態(tài)的空間邏輯。針對(duì)空間邏輯中的并發(fā)模態(tài)副詞是觀察進(jìn)程交互行為的關(guān)鍵因素,但引入并發(fā)模態(tài)副詞又導(dǎo)致模型檢測(cè)的不可判定性這一問(wèn)題。提出了一種可判定的、融合了空間模態(tài)和行為模態(tài)思想的應(yīng)用界程邏輯,并給出該邏輯在Applied-AC演算下的邏輯語(yǔ)義及模型檢測(cè)算法。本文還分析了Applied-AC演算進(jìn)程在應(yīng)用界程邏輯下的邏輯等價(jià)與結(jié)構(gòu)同余之間的包含關(guān)系,表明了運(yùn)用邏輯等價(jià)方式能夠以更抽象的層次來(lái)觀察進(jìn)程行為等價(jià)性質(zhì)。 3、提出了Applied-AC演算進(jìn)程在應(yīng)用界程邏輯下采用偏序方法進(jìn)行模型檢測(cè)的算法。本文分析了在應(yīng)用界程演算和應(yīng)用界程邏輯下采用偏序方法進(jìn)行模型檢測(cè)所面臨的問(wèn)題;研究了Applied-AC進(jìn)程偏序合流歸約應(yīng)具有的性質(zhì)以及影響進(jìn)程滿足偏序合流歸約的各種因素,從而給出了判別進(jìn)程偏序合流歸約的充分性條件。研究了應(yīng)用界程邏輯公式與進(jìn)程偏序合流歸約造成的進(jìn)程空間性質(zhì)變化之間的關(guān)系,得到空間邏輯公式對(duì)進(jìn)程偏序合流歸約行為不可觀察的充分性條件。給出判別在Applied-AC演算下進(jìn)行模型檢測(cè)中是否能夠運(yùn)用偏序方法來(lái)驗(yàn)證邏輯性質(zhì)的方法,及其實(shí)現(xiàn)算法。實(shí)驗(yàn)結(jié)果表明本文給出的算法在驗(yàn)證模型的死鎖性和安全性方面能夠較大程度上減輕狀態(tài)爆炸的現(xiàn)象。 4、給出了實(shí)現(xiàn)模型檢測(cè)系統(tǒng)的關(guān)鍵數(shù)據(jù)結(jié)構(gòu)和算法并實(shí)現(xiàn)了原型系統(tǒng)。進(jìn)程之間結(jié)構(gòu)同余關(guān)系的判定算法和數(shù)據(jù)結(jié)構(gòu)是實(shí)現(xiàn)空間模型檢測(cè)系統(tǒng)所面臨的主要問(wèn)題。Applied-AC演算引入帶參數(shù)的遞歸進(jìn)程和條件選擇進(jìn)程后,遞歸進(jìn)程的執(zhí)行將不再僅僅是單一進(jìn)程實(shí)例的簡(jiǎn)單重復(fù),在模型檢測(cè)器內(nèi)部進(jìn)程不能直接采用單一的樹型結(jié)構(gòu)來(lái)表示。針對(duì)這個(gè)問(wèn)題,本文設(shè)計(jì)了Applied-AC進(jìn)程的進(jìn)程等式系作為該進(jìn)程在模型檢測(cè)器內(nèi)部表示形式,從而將檢測(cè)進(jìn)程之間的結(jié)構(gòu)同余關(guān)系轉(zhuǎn)化為檢查進(jìn)程等式系之間的結(jié)構(gòu)等價(jià)關(guān)系。本文實(shí)現(xiàn)了模型檢測(cè)系統(tǒng)的原型系統(tǒng),通過(guò)實(shí)驗(yàn)證明了實(shí)現(xiàn)框架和算法的有效性。 總之,本文針對(duì)移動(dòng)界程演算在移動(dòng)計(jì)算系統(tǒng)形式化建模應(yīng)用中的關(guān)鍵問(wèn)題進(jìn)行了探索,取得一定的成果。對(duì)于提高移動(dòng)計(jì)算系統(tǒng)設(shè)計(jì)的可靠性,推動(dòng)移動(dòng)計(jì)算系統(tǒng)形式化建模應(yīng)用具有重要的理論和應(yīng)用價(jià)值。
【學(xué)位授予單位】：華南理工大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2010
【分類號(hào)】：TP338
【圖文】：

圖 2-1在通道界程系統(tǒng)中，每個(gè)主機(jī)都安裝有運(yùn)行時(shí)系統(tǒng)（RunningtimeSystem）來(lái)解移動(dòng)代理的通訊、移動(dòng)動(dòng)作等。計(jì)算實(shí)體之間的通訊、移動(dòng)交互原則：只有鄰近的計(jì)算實(shí)體之間才可以直接交是說(shuō)，LAN 內(nèi)主機(jī)不能直接與另一 LAN 中的主機(jī)交互，而必須借助于承擔(dān)網(wǎng)主機(jī)。類似地，移動(dòng)代理也不能直接與另一代理內(nèi)部的模塊直接交互，而需要理責(zé)任的代理；一個(gè)模塊也不能直接存取另一個(gè)模塊的內(nèi)部私有數(shù)據(jù)，而需要塊的接口。計(jì)算實(shí)體進(jìn)程的通訊、移動(dòng)交互都由命名的通道上完成。即主機(jī)之間由 TCP議提供的網(wǎng)絡(luò)信道來(lái)完成，移動(dòng)代理之間、或模塊之間由主機(jī)內(nèi)部網(wǎng)絡(luò)端口來(lái)2、通道界程演算通道界程演算（CA演算）是根據(jù)通道界程系統(tǒng)的通訊、交互方式，并在BoxedAm基礎(chǔ)上擴(kuò)展得到的演算模型。主要的語(yǔ)法和語(yǔ)義如下：

【參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 管旭東,楊怡玲,尤晉元;移動(dòng)灰箱演算中強(qiáng)干擾問(wèn)題的進(jìn)一步控制[J];軟件學(xué)報(bào);2002年05期

2 劉劍,林惠民;謂詞μ演算和模態(tài)圖的語(yǔ)義一致性[J];軟件學(xué)報(bào);2003年10期

本文編號(hào)：2768409