有界多態(tài)會話類型系統(tǒng)的研究.pdf

1、網(wǎng)絡(luò)技術(shù)和Web服務(wù)技術(shù)的廣泛應(yīng)用，推動和促進(jìn)了并行分布式計(jì)算的快速發(fā)展。并行分布式計(jì)算的主要特征包括并發(fā)性、分布性、實(shí)時(shí)性，具有這些復(fù)雜特征的并行分布式系統(tǒng)面臨著安全通信的挑戰(zhàn)。為了探索并行分布式系統(tǒng)的行為，確保并行分布式系統(tǒng)的安全通信，研究人員提出多個(gè)基于進(jìn)程間通信的、反映并發(fā)本質(zhì)的并發(fā)計(jì)算模型。如CSP模型、CCS模型、Pi-演算等。會話類型理論是繼上述程序設(shè)計(jì)模型之后提出的一個(gè)新的并發(fā)計(jì)算理論模型，它不僅繼承Pi-演算的基本語法

2、內(nèi)容以及用歸約表示進(jìn)程間通信的思想，而且引入了類型的理論，從而能夠更好地結(jié)構(gòu)化并推理進(jìn)程間的通信行為，捕捉通信進(jìn)程之間的協(xié)議規(guī)范;會話類型理論的類型指派規(guī)則可以轉(zhuǎn)化為一種實(shí)際的類型檢測算法，因此會話類型理論成為了一種有效的推理通信行為的形式化方法。
　　本研究主要內(nèi)容包括：⑴會話類型理論是在Pi-演算的基礎(chǔ)上提出來的，它繼承了Pi-演算語法簡明和用歸約表達(dá)進(jìn)程間通信的優(yōu)點(diǎn)，在原始的會話類型系統(tǒng)中，通道和變量被統(tǒng)一命名為名字進(jìn)行傳遞

3、，這樣的缺點(diǎn)是無法很好的體現(xiàn)出數(shù)據(jù)和通道的傳遞過程，因此在結(jié)合前人研究的有界多態(tài)會話類型系統(tǒng)理論的基礎(chǔ)上，本文提出一個(gè)基于Delegation的有界多態(tài)會話類型系統(tǒng)，即該系統(tǒng)將數(shù)據(jù)傳遞和通道傳遞區(qū)分開來，分別定義數(shù)據(jù)傳遞和通道傳遞的語法、操作語義與類型指派規(guī)則。⑵為了更好地反映消息傳遞過程中通道會話類型的改變，本文對原始會話類型系統(tǒng)的環(huán)境做了改進(jìn)，增加了通道環(huán)境C，將原來的類型指派規(guī)則的判定形式由△;Γ(F)P改進(jìn)為△;Γ(F)P(△)