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

来源 :浙江师范大学 | 被引量 : 0次 | 上传用户:qwer32173
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
随着计算机网络及通信技术的发展,以分布性、并发性、异构性和互操作性等为主要特征的并发分布式计算已成为计算机研究中的主流方向。确保并行分布式系统进行安全交互的结构化通信,是并发分布式计算理论和实践的中心问题。基于Pi-演算的会话类型理论为结构化通信提供了理论基础,是结构化交互和解释通信行为的一种有效的形式化方法。在分布式计算场景中,存在大量通过消息传递进行通信的程序,会话类型理论能够验证传递消息的结构和序列,并分析其与协议描述是否一致。以会话类型理论为基础的类型系统,是研究如何将编程语言中的数值和表达式归为类型,以及类型之间互相作用的形式化方法。类型系统能够分析和禁止程序中非正常的行为,避免发生运行时错误,确保语言的安全性。会话类型理论及类型系统,是以通信为中心的分布式程序设计研究的关键问题。本文的工作主要围绕有界多态的类型系统中,描述无限次重复行为、同步和异步通信中保持演进特性,以及异步交互序列的局部优化等问题而展开,其主要研究内容及贡献如下:(1)研究了会话类型和Pi-演算的当前工作以及已有的类型系统,提出带有递归类型的有界多态类型系统。递归会话类型允许协议描述不定次数的重复行为,在客户机-服务器交互模式中,服务器端进程不仅能提供一次服务,而且能提供任意次数的服务,提高了系统的灵活性。同时,结合会话类型子类型,定义了松弛对偶关系,该关系不仅使得通信两端交互的类型更加灵活,而且有助于定义类型一致性则和研究演进特性。此外,递归会话类型本身是会话类型的一种,因此定义了递归会话类型的子类型及其松弛的对偶关系。(2)研究了演进特性分别在同步和异步通信中的保持,并证明了系统可靠性和通信安全性。通道类型被区分为共享通道和活动通道,并分析了在同步和异步环境下,以及在不同类型通道中,可能产生死锁的情形。进一步地,分析了产生死锁的原因并给出了解除死锁的方法,结合松弛的对偶关系定义了类型一致性法则等法则,确保类型系统保持演进特性。此外,证明类型系统保持主题归约理论、类型安全理论和演进特性等,确保了系统可靠性和通信安全性。(3)特别地,对于部分可交换的异步二元会话及多元会话,通过引入异步通信子类型,使每一位参与者上的动作序列可以进行排列和局部优化,提高通信效率的同时,有效地解除了通信过程中发生的死锁。此外,消息类型被区分成依赖和非依赖的类型,并分别定义了动作异步子类型指派规则。同时,由于异步动作排列和优化将改变接收和发送消息的序列和结构,为了确保通信安全性,本文通过具体例子揭示了其中产生死锁的情形,并保持了演进特性。此外,为了使动作排列自动化,结合会话类型的子类型和异步通信子类型两个概念,呈现了的算法化的异步子类型。
其他文献
学位
微学习是一种新型学习方式,是在线学习适应碎片化时代的一种发展形式。微学习最主要的特点是,其学习单元包含的知识内容相对精简,构成包括文本、音频/视频和图像等多种形式,
近年来,随着计算机技术、网络传输技术和视频压缩技术的不断发展,人们对生产和生活环境的安全要求不断提高,视频监控系统以其直观、方便、信息内容丰富的特点已越来越受到人们的
近年来,计算机网络环境日益复杂,网络战在国家安全中地位迅速提升;另外,木马和僵尸网络有逐年快速增加的趋势,带动黑色产业链进一步蔓延。通过对木马控制模型及检测技术进行
学位
微尺度海洋湍流混合是大洋中普遍存在的现象,湍流混合是整个大洋环流的源动力,同时是控制着海洋生态环境的关键因素,对于海水的能量、质量、动量和全球温度气候也有重要影响。研
随着互联网的普及,越来越多的多媒体信息通过互联网传播,IPTV (Internet Protocol Television)直播服务就是其中一类。IPTV直播服务具有较高的服务质量(Quality of Service,
路网中的空间路径搜索是地图服务中的一项基本功能,有别于传统的最短路径搜索,基于关键词的最优路径搜索(Keyword-aware Optimal Route Search,KORS)旨在查询返回一条覆盖所
学位
随着计算机网络的飞速发展,使用无线局域网(WLAN)的用户也日益增多,面向WLAN的网络安全研究也受到越来越多的重视。入侵检测和防御技术作为网络安全防护的重要手段,在传统有线网