離散實(shí)時(shí)Mobile Ambients.pdf

1、隨著計(jì)算機(jī)技術(shù)和網(wǎng)絡(luò)技術(shù)的發(fā)展，移動(dòng)計(jì)算與實(shí)時(shí)計(jì)算已經(jīng)成為計(jì)算機(jī)科學(xué)領(lǐng)域的兩個(gè)研究熱點(diǎn)，受到越來(lái)越多的關(guān)注。不同領(lǐng)域的學(xué)者對(duì)這一問(wèn)題的研究有不同的方法。形式化方法作為研究分布式、并發(fā)計(jì)算的一個(gè)重要重要方法，近年來(lái)得到了飛速的發(fā)展。形式化專(zhuān)家們提出了許多移動(dòng)計(jì)算和實(shí)時(shí)計(jì)算的形式系統(tǒng)：如自動(dòng)機(jī)、petri 網(wǎng)、CCS、Pi 演算、Mobile Ambients 等．這些形式系統(tǒng)可以刻畫(huà)、研究并發(fā)分布式系統(tǒng)，傳值計(jì)算以及空間移動(dòng)系統(tǒng)。但是它們

2、各有特色，比方說(shuō)Pi演算適合于傳值計(jì)算；而Mobile Ambients在空間移動(dòng)計(jì)算系統(tǒng)中更能夠發(fā)揮自己的優(yōu)勢(shì)。實(shí)時(shí)計(jì)算作為近年計(jì)算機(jī)科學(xué)領(lǐng)域的另一個(gè)研究的熱點(diǎn)，形式化專(zhuān)家也提出了它的形式化框架．這些實(shí)時(shí)形式化框架主要是用時(shí)間對(duì)原有的形式系統(tǒng)的擴(kuò)展。新的形式化框架能夠研究計(jì)算機(jī)系統(tǒng)在時(shí)間方面的性質(zhì)，已有的實(shí)時(shí)系統(tǒng)有Timed Automata，Timed CCS，實(shí)時(shí)Pi演算等，但這些實(shí)時(shí)形式系統(tǒng)由于擴(kuò)展前原型系統(tǒng)的局限性，不能表示空

3、間結(jié)構(gòu)。通過(guò)以MobileAmbients演算為基礎(chǔ)的實(shí)時(shí)擴(kuò)充，可以很好的將時(shí)空統(tǒng)一到同一個(gè)形式化框架中研究。 本文首先討論了Mobile Ambients 的優(yōu)點(diǎn)和不足，然后提出一種基于圖的實(shí)時(shí)移動(dòng)計(jì)算模型，接下來(lái)用時(shí)間對(duì)Mobile Ambients進(jìn)行擴(kuò)展，提出了一種新的實(shí)時(shí)形式化系統(tǒng)——離散實(shí)時(shí) MobileAmbients。對(duì)一個(gè)系統(tǒng)作模型驗(yàn)證，不僅需要將系統(tǒng)用形式語(yǔ)言表示，而且還要將系統(tǒng)要求滿(mǎn)足的性質(zhì)表示成模態(tài)邏輯公

4、式。為利用離散實(shí)時(shí) Mobile Ambients 對(duì)實(shí)時(shí)移動(dòng)計(jì)算系統(tǒng)做模型驗(yàn)證，本文對(duì)NobileAmbients 的時(shí)態(tài)邏輯也作了擴(kuò)展，提出了能夠描述實(shí)時(shí)性質(zhì)的模態(tài)邏輯。最后對(duì)離散實(shí)時(shí)Mobile Ambients演算的子集提出了模型驗(yàn)證算法，并且用離散實(shí)時(shí) Mobile Ambients 演算建模Web服務(wù)組合語(yǔ)言BPEL4WS。 本文的主要內(nèi)容包括以下幾個(gè)部分： 第一，討論了mobile ambients 的優(yōu)缺

5、點(diǎn)，并且提出了基于圖的實(shí)時(shí)移動(dòng)計(jì)算模型； 第二，對(duì)Mobile Ambients 作實(shí)時(shí)擴(kuò)展，提出新的實(shí)時(shí)形式系統(tǒng)——離散實(shí)時(shí) Mobile Ambients； 第三，提出離散實(shí)時(shí)Mobile Ambients演算的時(shí)態(tài)邏輯，給出離散實(shí)時(shí)Mobile Ambients的模型驗(yàn)證算法，并給出離散實(shí)時(shí)MobileAmbients 演算模型驗(yàn)證的可判定性的證明。 第四，利用離散實(shí)時(shí) Mobile Ambients 建模