客户机—服务器交互模式类型系统的演进特性研究

发布时间：2018-02-23 13:15

本文关键词： 移动进程演算 Pi-演算类型理论类型系统有界多态性部分可交换性演进特性　出处：《浙江师范大学》2013年硕士论文　论文类型：学位论文

【摘要】：随着计算机网络及通信技术的发展,以分布性、并发性、异构性和互操作性等为主要特征的并发分布式计算已成为计算机研究中的主流方向。确保并行分布式系统进行安全交互的结构化通信,是并发分布式计算理论和实践的中心问题。基于Pi-演算的会话类型理论为结构化通信提供了理论基础,是结构化交互和解释通信行为的一种有效的形式化方法。在分布式计算场景中,存在大量通过消息传递进行通信的程序,会话类型理论能够验证传递消息的结构和序列,并分析其与协议描述是否一致。以会话类型理论为基础的类型系统,是研究如何将编程语言中的数值和表达式归为类型,以及类型之间互相作用的形式化方法。类型系统能够分析和禁止程序中非正常的行为,避免发生运行时错误,确保语言的安全性。会话类型理论及类型系统,是以通信为中心的分布式程序设计研究的关键问题。本文的工作主要围绕有界多态的类型系统中,描述无限次重复行为、同步和异步通信中保持演进特性,以及异步交互序列的局部优化等问题而展开,其主要研究内容及贡献如下： (1)研究了会话类型和Pi-演算的当前工作以及已有的类型系统,提出带有递归类型的有界多态类型系统。递归会话类型允许协议描述不定次数的重复行为,在客户机-服务器交互模式中,服务器端进程不仅能提供一次服务,而且能提供任意次数的服务,提高了系统的灵活性。同时,结合会话类型子类型,定义了松弛对偶关系,该关系不仅使得通信两端交互的类型更加灵活,而且有助于定义类型一致性则和研究演进特性。此外,递归会话类型本身是会话类型的一种,因此定义了递归会话类型的子类型及其松弛的对偶关系。 (2)研究了演进特性分别在同步和异步通信中的保持,并证明了系统可靠性和通信安全性。通道类型被区分为共享通道和活动通道,并分析了在同步和异步环境下,以及在不同类型通道中,可能产生死锁的情形。进一步地,分析了产生死锁的原因并给出了解除死锁的方法,结合松弛的对偶关系定义了类型一致性法则等法则,确保类型系统保持演进特性。此外,证明类型系统保持主题归约理论、类型安全理论和演进特性等,确保了系统可靠性和通信安全性。 (3)特别地,对于部分可交换的异步二元会话及多元会话,通过引入异步通信子类型,使每一位参与者上的动作序列可以进行排列和局部优化,提高通信效率的同时,有效地解除了通信过程中发生的死锁。此外,消息类型被区分成依赖和非依赖的类型,并分别定义了动作异步子类型指派规则。同时,由于异步动作排列和优化将改变接收和发送消息的序列和结构,为了确保通信安全性,本文通过具体例子揭示了其中产生死锁的情形,并保持了演进特性。此外,为了使动作排列自动化,结合会话类型的子类型和异步通信子类型两个概念,呈现了的算法化的异步子类型。
[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.

【学位授予单位】：浙江师范大学
【学位级别】：硕士
【学位授予年份】：2013
【分类号】：TP301.2

【共引文献】