有界多态会话类型系统的研究

发布时间：2018-05-09 15:48

本文选题：Pi-演算 + 会话类型　；参考：《浙江师范大学》2014年硕士论文

【摘要】：网络技术和Web服务技术的广泛应用,推动和促进了并行分布式计算的快速发展。并行分布式计算的主要特征包括并发性、分布性、实时性,具有这些复杂特征的并行分布式系统面临着安全通信的挑战。为了探索并行分布式系统的行为,确保并行分布式系统的安全通信,研究人员提出多个基于进程间通信的、反映并发本质的并发计算模型。如CSP模型、CCS模型、Pi-演算等。会话类型理论是继上述程序设计模型之后提出的一个新的并发计算理论模型,它不仅继承Pi-演算的基本语法内容以及用归约表示进程间通信的思想,而且引入了类型的理论,从而能够更好地结构化并推理进程间的通信行为,捕捉通信进程之间的协议规范；会话类型理论的类型指派规则可以转化为一种实际的类型检测算法,因此会话类型理论成为了一种有效的推理通信行为的形式化方法。本文的主要工作是首先介绍了会话类型系统的基础理论和基本框架结构,然后在原有的有界多态会话类型系统的基础上对其原有的传递消息机制做了改进,最后用例子阐述本文工作的意义。本文的主要贡献如下： (1)会话类型理论是在Pi-演算的基础上提出来的,它继承了Pi-演算语法简明和用归约表达进程间通信的优点,在原始的会话类型系统中,通道和变量被统一命名为名字进行传递,这样的缺点是无法很好的体现出数据和通道的传递过程,因此在结合前人研究的有界多态会话类型系统理论的基础上,本文提出一个基于Delegation的有界多态会话类型系统,即该系统将数据传递和通道传递区分开来,分别定义数据传递和通道传递的语法、操作语义与类型指派规则。 (2)为了更好地反映消息传递过程中通道会话类型的改变,本文对原始会话类型系统的环境做了改进,增加了通道环境C,将原来的类型指派规则的判定形式由△；r├P改进为△；Г├P(?)C,使得新定义的类型指派规则不仅可以很好地追踪通道使用的顺序,而且能够清晰地反映消息传递过程中通道会话类型的改变,进而更直接地表达各种消息传递的过程。 (3)安全性是会话类型系统最基本的性质。所谓安全性是指良类型的进程可以进行任何序列的归约步骤而不会发生错误。本文从主体归约和类型安全两个方面证明了此类型系统的安全性。之后,我们用实例展示了用会话类型理论来描述消息传递的过程,同时反映消息传递过程中通道类型的改变。
[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

【参考文献】