本文選題：Pi-演算 + 會話類型�。� 參考：《浙江師范大學》2014年碩士論文

【摘要】：網(wǎng)絡(luò)技術(shù)和Web服務(wù)技術(shù)的廣泛應用,推動和促進了并行分布式計算的快速發(fā)展。并行分布式計算的主要特征包括并發(fā)性、分布性、實時性,具有這些復雜特征的并行分布式系統(tǒng)面臨著安全通信的挑戰(zhàn)。為了探索并行分布式系統(tǒng)的行為,確保并行分布式系統(tǒng)的安全通信,研究人員提出多個基于進程間通信的、反映并發(fā)本質(zhì)的并發(fā)計算模型。如CSP模型、CCS模型、Pi-演算等。會話類型理論是繼上述程序設(shè)計模型之后提出的一個新的并發(fā)計算理論模型,它不僅繼承Pi-演算的基本語法內(nèi)容以及用歸約表示進程間通信的思想,而且引入了類型的理論,從而能夠更好地結(jié)構(gòu)化并推理進程間的通信行為,捕捉通信進程之間的協(xié)議規(guī)范；會話類型理論的類型指派規(guī)則可以轉(zhuǎn)化為一種實際的類型檢測算法,因此會話類型理論成為了一種有效的推理通信行為的形式化方法。 本文的主要工作是首先介紹了會話類型系統(tǒng)的基礎(chǔ)理論和基本框架結(jié)構(gòu),然后在原有的有界多態(tài)會話類型系統(tǒng)的基礎(chǔ)上對其原有的傳遞消息機制做了改進,最后用例子闡述本文工作的意義。本文的主要貢獻如下： (1)會話類型理論是在Pi-演算的基礎(chǔ)上提出來的,它繼承了Pi-演算語法簡明和用歸約表達進程間通信的優(yōu)點,在原始的會話類型系統(tǒng)中,通道和變量被統(tǒng)一命名為名字進行傳遞,這樣的缺點是無法很好的體現(xiàn)出數(shù)據(jù)和通道的傳遞過程,因此在結(jié)合前人研究的有界多態(tài)會話類型系統(tǒng)理論的基礎(chǔ)上,本文提出一個基于Delegation的有界多態(tài)會話類型系統(tǒng),即該系統(tǒng)將數(shù)據(jù)傳遞和通道傳遞區(qū)分開來,分別定義數(shù)據(jù)傳遞和通道傳遞的語法、操作語義與類型指派規(guī)則。 (2)為了更好地反映消息傳遞過程中通道會話類型的改變,本文對原始會話類型系統(tǒng)的環(huán)境做了改進,增加了通道環(huán)境C,將原來的類型指派規(guī)則的判定形式由△；r├P改進為△；Г├P(?)C,使得新定義的類型指派規(guī)則不僅可以很好地追蹤通道使用的順序,而且能夠清晰地反映消息傳遞過程中通道會話類型的改變,進而更直接地表達各種消息傳遞的過程。 (3)安全性是會話類型系統(tǒng)最基本的性質(zhì)。所謂安全性是指良類型的進程可以進行任何序列的歸約步驟而不會發(fā)生錯誤。本文從主體歸約和類型安全兩個方面證明了此類型系統(tǒng)的安全性。之后,我們用實例展示了用會話類型理論來描述消息傳遞的過程,同時反映消息傳遞過程中通道類型的改變。
[Abstract]:The wide application of network technology and Web services technology has promoted the rapid development of parallel distributed computing. The main features of parallel distributed computing include concurrency, distribution and real-time. Parallel distributed systems with these complex features face the challenge of secure communication. In order to explore the behavior of parallel distributed systems and ensure the secure communication of parallel distributed systems, researchers proposed several concurrent computing models based on inter-process communication, which reflect the nature of concurrency. For example, CSP model, CSP model and Pi-calculus, etc. The theory of session type is a new concurrent computing model proposed after the above programming model. It not only inherits the basic grammatical content of Pi-calculus and the idea of using reduction to represent inter-process communication, but also introduces the theory of type. Thus, the communication behavior between processes can be better structured and inferred, and the protocol specification between communication processes can be captured, and the type assignment rules of session type theory can be transformed into an actual type detection algorithm. Therefore, the theory of conversation type has become an effective formal method of reasoning communication behavior. The main work of this paper is to introduce the basic theory and basic framework of the session type system, and then improve the original message delivery mechanism based on the original bounded polymorphic session type system. Finally, an example is given to illustrate the significance of this work. The main contributions of this paper are as follows: The theory of session type is based on Pi-calculus. It inherits the advantages of concise syntax and reduced representation of inter-process communication in Pi-Calculus. In the original session type system, channels and variables are uniformly named for transmission. Such a disadvantage is that it can not well reflect the data and channel transfer process. Therefore, based on the theory of bounded polymorphic session type system, a bounded polymorphic session type system based on Delegation is proposed in this paper. That is, the system distinguishes data transfer from channel transfer, defines syntax of data transfer and channel transfer, operation semantics and type assignment rules respectively. 2) in order to better reflect the change of channel session type during message passing, this paper improves the environment of the original session type system. With the addition of channel environment C, the decision form of the original type assignment rule is improved from r / P to C, so that the newly defined type assignment rule can not only trace the order of channel usage well, Moreover, it can clearly reflect the change of channel session type in the process of message passing, and then express all kinds of message passing process more directly. Security is the most basic property of a session type system. Security means that a good-type process can perform any sequence reduction step without error. This paper proves the security of this type system from two aspects: principal reduction and type safety. Then we illustrate the process of message passing with the theory of session type and reflect the change of channel type in the process of message passing.
【學位授予單位】：浙江師范大學
【學位級別】：碩士
【學位授予年份】：2014
【分類號】：TP393.09

【參考文獻】

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

1 蔣慧,張興元,王元元,謝希仁;類型系統(tǒng)的構(gòu)造、實現(xiàn)及其在程序設(shè)計語言中的應用[J];南京大學學報(自然科學版);2001年02期

2 周曉聰;李文軍;李師賢;;類型系統(tǒng)的研究與進展[J];計算機科學;2000年05期

，

本文編號：1866609