学位论文 > 优秀研究生学位论文题录展示

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

作 者: 杨振国
导 师: 钟发荣
学 校: 浙江师范大学
专 业: 计算机软件与理论
关键词: 移动进程演算 Pi-演算 类型理论 类型系统 有界多态性 部分可交换性 演进特性
分类号: TP301.2
类 型: 硕士论文
年 份: 2013年
下 载: 11次
引 用: 0次
阅 读: 论文下载
 

内容摘要


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

全文目录


摘要  3-5
ABSTRACT  5-8
目录  8-10
第一章 绪论  10-16
  1.1 选题背景  10-11
  1.2 国内外研究现状  11-14
    1.2.1 结构化通信  11-12
    1.2.2 移动进程演算  12-13
    1.2.3 会话类型理论  13-14
  1.3 本文的主要工作  14-15
  1.4 本文的组织结构  15-16
第二章 会话类型理论及Pi-演算简述  16-25
  2.1 会话类型简述  16-19
    2.1.1 会话类型  16-17
    2.1.2 会话类型子类型  17-18
    2.1.3 有界多态性  18-19
  2.2 演进理论  19-20
  2.3 部分可交换的异步会话  20-21
  2.4 Pi-演算简述  21-24
    2.4.1 基本语法  21-22
    2.4.2 操作语义及同余关系  22-24
  2.5 小结  24-25
第三章 客户机-服务器交互模式类型系统的基础构造  25-34
  3.1 语法和概念  25-28
    3.1.1 类型  25-27
    3.1.2 进程  27-28
  3.2 会话类型子类型指派规则  28-30
  3.3 类型指派规则  30-32
  3.4 可操作语义  32-33
  3.5 小结  33-34
第四章 类型系统中部分可交换的异步会话  34-43
  4.1 异步通信子类型及其消息依赖性  34-37
    4.1.1 二元会话中的异步通信子类型  34-36
    4.1.2 多元会话中的异步通信子类型  36-37
  4.2 非递归会话类型的可交换异步子类型  37-39
  4.3 递归会话类型的可交换异步子类型  39-40
  4.4 算法化的异步子类型指派  40-41
  4.5 小结  41-43
第五章 同步及异步会话类型系统的可靠性和通信安全性  43-52
  5.1 类型系统可靠性  43-46
    5.1.1 主题归约理论  43-45
    5.1.2 类型安全理论  45-46
  5.2 同步通信安全性  46-49
    5.2.1 同步通信中的死锁情形  46-48
    5.2.2 演进特性的保持  48-49
  5.3 异步通信安全性  49-51
    5.3.1 异步通信中的死锁情形  49-50
    5.3.2 演进特性的保持  50-51
  5.4 小结  51-52
第六章 总结与展望  52-54
  6.1 工作总结  52-53
  6.2 工作展望  53-54
参考文献  54-59
攻读学位期间取得的研究成果  59-60
致谢  60-62

相似论文

  1. 从文本类型理论看“动态对等”与当代圣经汉译,H315.9
  2. 基于应用PI演算的远程网络投票协议安全性自动化证明,TP393.08
  3. 基于人职匹配模型的卫生人力资源信息服务网站的研究与设计,R-4
  4. Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
  5. 基于文本类型理论的企业简介汉英翻译研究,H315.9
  6. 功能目的论视角下《孙子兵法》英译本对比分析,H315.9
  7. 基于进程代数的面向服务软件体系结构建模,TP393.09
  8. 基于Pi演算的网格工作流形式化描述及有效性检测,TP311.52
  9. 基于PI演算的CRM系统的设计与实现,TP311.52
  10. 从功能翻译理论视角谈学术论文摘要的英译,H315.9
  11. 刑法中的类推,D914
  12. 洛伦兹类型系统动力行为分析,O19
  13. 感性的人道内涵,I516
  14. 德国功能论视角下《京华烟云》两中译本对比研究,I046
  15. 新疆抗震安居工程砖木房屋振动台试验研究与理论分析,TU317
  16. 基于自治与协商机制的柔性制造车间智能调度技术研究,TH165
  17. 基于用户行为的下一代移动互联网络若干关键问题的研究,TP393.02
  18. 水下机器人协同仿真模型组合方法的研究,TP242
  19. 功能翻译理论框架下的本地化翻译研究-以SPS(Stoner管道模拟器)软件翻译为例,H059
  20. 基于诺德文本类型理论的口译策略研究-以2009-2012年温家宝总理“两会”记者招待会口译为例,H059
  21. 《全球交流下的文化与政治》(第六章)翻译报告,H315.9

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 一般性问题 > 理论、方法 > 形式语言理论
© 2012 www.xueweilunwen.com