本文關(guān)鍵詞： 移動(dòng)進(jìn)程演算 Pi-演算 類型理論 類型系統(tǒng) 有界多態(tài)性 部分可交換性 演進(jìn)特性　出處：《浙江師范大學(xué)》2013年碩士論文　論文類型：學(xué)位論文

【摘要】：隨著計(jì)算機(jī)網(wǎng)絡(luò)及通信技術(shù)的發(fā)展,以分布性、并發(fā)性、異構(gòu)性和互操作性等為主要特征的并發(fā)分布式計(jì)算已成為計(jì)算機(jī)研究中的主流方向。確保并行分布式系統(tǒng)進(jìn)行安全交互的結(jié)構(gòu)化通信,是并發(fā)分布式計(jì)算理論和實(shí)踐的中心問題�；赑i-演算的會(huì)話類型理論為結(jié)構(gòu)化通信提供了理論基礎(chǔ),是結(jié)構(gòu)化交互和解釋通信行為的一種有效的形式化方法。在分布式計(jì)算場景中,存在大量通過消息傳遞進(jìn)行通信的程序,會(huì)話類型理論能夠驗(yàn)證傳遞消息的結(jié)構(gòu)和序列,并分析其與協(xié)議描述是否一致。以會(huì)話類型理論為基礎(chǔ)的類型系統(tǒng),是研究如何將編程語言中的數(shù)值和表達(dá)式歸為類型,以及類型之間互相作用的形式化方法。類型系統(tǒng)能夠分析和禁止程序中非正常的行為,避免發(fā)生運(yùn)行時(shí)錯(cuò)誤,確保語言的安全性。會(huì)話類型理論及類型系統(tǒng),是以通信為中心的分布式程序設(shè)計(jì)研究的關(guān)鍵問題。 本文的工作主要圍繞有界多態(tài)的類型系統(tǒng)中,描述無限次重復(fù)行為、同步和異步通信中保持演進(jìn)特性,以及異步交互序列的局部優(yōu)化等問題而展開,其主要研究內(nèi)容及貢獻(xiàn)如下： (1)研究了會(huì)話類型和Pi-演算的當(dāng)前工作以及已有的類型系統(tǒng),提出帶有遞歸類型的有界多態(tài)類型系統(tǒng)。遞歸會(huì)話類型允許協(xié)議描述不定次數(shù)的重復(fù)行為,在客戶機(jī)-服務(wù)器交互模式中,服務(wù)器端進(jìn)程不僅能提供一次服務(wù),而且能提供任意次數(shù)的服務(wù),提高了系統(tǒng)的靈活性。同時(shí),結(jié)合會(huì)話類型子類型,定義了松弛對偶關(guān)系,該關(guān)系不僅使得通信兩端交互的類型更加靈活,而且有助于定義類型一致性則和研究演進(jìn)特性。此外,遞歸會(huì)話類型本身是會(huì)話類型的一種,因此定義了遞歸會(huì)話類型的子類型及其松弛的對偶關(guān)系。 (2)研究了演進(jìn)特性分別在同步和異步通信中的保持,并證明了系統(tǒng)可靠性和通信安全性。通道類型被區(qū)分為共享通道和活動(dòng)通道,并分析了在同步和異步環(huán)境下,以及在不同類型通道中,可能產(chǎn)生死鎖的情形。進(jìn)一步地,分析了產(chǎn)生死鎖的原因并給出了解除死鎖的方法,結(jié)合松弛的對偶關(guān)系定義了類型一致性法則等法則,確保類型系統(tǒng)保持演進(jìn)特性。此外,證明類型系統(tǒng)保持主題歸約理論、類型安全理論和演進(jìn)特性等,確保了系統(tǒng)可靠性和通信安全性。 (3)特別地,對于部分可交換的異步二元會(huì)話及多元會(huì)話,通過引入異步通信子類型,使每一位參與者上的動(dòng)作序列可以進(jìn)行排列和局部優(yōu)化,提高通信效率的同時(shí),有效地解除了通信過程中發(fā)生的死鎖。此外,消息類型被區(qū)分成依賴和非依賴的類型,并分別定義了動(dòng)作異步子類型指派規(guī)則。同時(shí),由于異步動(dòng)作排列和優(yōu)化將改變接收和發(fā)送消息的序列和結(jié)構(gòu),為了確保通信安全性,本文通過具體例子揭示了其中產(chǎn)生死鎖的情形,并保持了演進(jìn)特性。此外,為了使動(dòng)作排列自動(dòng)化,結(jié)合會(huì)話類型的子類型和異步通信子類型兩個(gè)概念,呈現(xiàn)了的算法化的異步子類型。
[Abstract]:With the development of computer network and communication technology, the distribution, concurrency, heterogeneity and interoperability as the main characteristics of concurrent distributed computing has become the mainstream direction of computer research. To ensure the safety of interactive parallel distributed structured communication system, is the center problem of concurrent distributed computing theory and practice. The session type theory based on Pi- calculus provides a theoretical basis for structured communication, is an effective formal method of structured interaction and explain communication behavior in distributed computing. In the scene, there are a lot of communication through message transfer procedures, session type structure and sequence verification theory can deliver the message, and the protocol description and analysis of whether consistent. Type system to session types based on the theory, the research on how to apply the numerical expressions and in programming languages belong to the type and class Formal method of interaction between type. The type system to abnormal behavior analysis and the prohibition of the procedure, to avoid the occurrence of runtime errors, ensure the safety of the language. The session type theory and the type system, it is a key problem in distributed programming communication as the center.
The work of this paper is mainly focused on the description of the infinite repeated behavior, the evolution characteristics in synchronous and asynchronous communication, and the local optimization of asynchronous interaction sequence.
(1) the study session type and calculation of Pi- current work and the existing type system, the polymorphic type system with bounded recursive types. Repetitive behavior types allow recursive session protocol description an indefinite number of times, in a client server model, the server process can not only provide a service, but also can provide any number of services, improve the flexibility of the system. At the same time, combined with the session type sub type, defines the relationship between dual relaxation of relations, not only makes the type of both sides of the communication interaction is more flexible, but also helps to define the type of consistency and Research on the evolution characteristics. In addition, the recursive session type itself is a type of conversation therefore, the definition of recursive session type and its dual relaxation.
(2) study the evolution characteristics were maintained in synchronous and asynchronous communication, and proved the reliability of the system and the communication security. The channel type is divided into shared channel and channel activities, and analyzes on the synchronous and asynchronous environments, and in different types of channels, which may produce deadlock situations. Further, analysis of the cause of the deadlock and gives the method to relieve the deadlock, combined with the relaxation of the dual relationship defines a type consistency rule rule, ensure that the type system evolution characteristics. In addition, the proof of the type system to keep the subject reduction theory, type theory and the evolution of safety characteristics, to ensure the reliability of the system and the communication security.
(3) in particular, the asynchronous part can be exchange two yuan session and multiple sessions, by introducing asynchronous communication sub types, the action sequence of each participant can be arranged and the local optimization, and improve communication efficiency, effectively relieve the deadlock in the process of communication. In addition, the message type is area is divided into independent and dependent types, and define the different types of action steps assignment rules. At the same time, the sequence and structure arrangement and optimization of asynchronous action will change the sending and receiving of messages, in order to ensure the security of communication, through specific examples reveals the deadlock situation, and maintain the evolution characteristics. In addition in order to make the arrangement of action, automation, combined with two session type and sub type of asynchronous communication, presents the algorithm of asynchronous sub type.

【學(xué)位授予單位】：浙江師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2013
【分類號】：TP301.2

【共引文獻(xiàn)】

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

1 辜希武;李瑞軒;盧正鼎;;Web服務(wù)組合規(guī)范WS-CDL的類型化形式化模型(英文)[J];Journal of Southeast University(English Edition);2008年03期

2 辜希武;盧正鼎;;類型化的Web服務(wù)組合形式化模型[J];計(jì)算機(jī)科學(xué);2008年01期

相關(guān)博士學(xué)位論文 前2條

1 李德勝;基于Pi演算的Web服務(wù)組合研究[D];北京郵電大學(xué);2011年

2 辜希武;Web服務(wù)組合形式化模型研究[D];華中科技大學(xué);2007年

相關(guān)碩士學(xué)位論文 前1條

1 王博;基于網(wǎng)絡(luò)的實(shí)訓(xùn)室管理系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[D];河北科技大學(xué);2010年

，

本文編號：1526726