基于Pi演算的Web服务组合研究

论文摘要

近年来,随着SOA架构和Web服务的广泛深入,如何将Web服务组合按照不同的目标、方式进行组合成为了人们关注的热点。虽然人们对Web服务以及Web服务组合已经有比较充分的研究并且已经付诸实践,但是从Web服务及其组合的研究现状来开,在很大程度上都还停留在非形式化或者半形式化的基础上。另一方面,形式化方法本身对Web服务组合的整个生命周期（即服务定义,服务发现,服务组合,服务验证）都有很好的指导和支持作用。反之,对于形式化方法来说也需要找到其合适的应用场景,并且在对应用的研究中逐步发展和改进自身。本文致力于用扩展的Pi演算对Web服务组合生命周期中各个时期的关键问题进行形式化描述和分析,包括设计时刻的建模、运行时刻的验证、选择时刻的服务选择等。具体来说,主要工作和创新主要包括如下若干方面：（1）针对服务组合的特征,对传统的Pi演算扩展为Pi-beam,包括语法扩展、语义、类型系统等扩展方面。其中语法扩展有带约束的束通道、逻辑并行和逻辑选择；语义扩展有束通道链接语义规则、逻辑并行和逻辑选择的转化规则等；类型扩展包括增加带约束的束通道类型和相关的类型化规则和类型错误规则。（2）为了利用Pi-beam的相关特性并且直观地表示Web服务组合系统的静态特征,我们开发了带标注的进程链接图和它的简化版本,并用它们对Web服务组合中的基本控制流模式进行了统一化的建模。（3）利用Pi-beam的类型系统和规约特性,我们讨论了服务组合的验证问题。类型正确性验证,主要是以进程是否属于良好类型或者推导出错误为依据。根据Pi-beam演化后的形式,可以判断一个组合进程时候是流程正确或者错误。在流程错误的例子中,死锁和活锁问题被重点讨论。尤其是对死锁问题,笔者通过对Pi-beam演算中的进程类型进行进一步扩展,使得组合后的进程表达式的类型可以用于判断死锁甚至是避免死锁。（4）另外一种基于流程正确性的自动组合算法被提出。它基于Pi-beam演算的语义规则的模式匹配,但不需要复杂的定理证明器和推理工具的介入,在时间复杂度上,由于类型的引入,使得搜索空间大幅减少。（5）由于QoS感知的服务组合已经被证明是NP-困难问题,因此大量的启发式算法被用到其上。粒子群优化（PSO）算法是近年来研究得比较多的方法之一。然而大多数研究仅仅局限于怎样使用这类算法和讨论算法的效率,对方法本身的形式化模型讨论的很少。本文在$-代数的启发下,针对PSO这一具体的方法,对Pi-beam演算进行了非功能性扩展,引入了计算QoS和根据QoS进行选择的原语和规则,并且引入了PSO的元搜索过程作为原语。在这个代数的基础上,开发了在抽象语法树基础上的QoS估值算法,并进行了模拟仿真实验。（6）基于在云计算和云服务的实践需要,笔者对Pi-beam演算扩展成高阶分布式Pi演算,它支持类似Lambda演算中的抽象和应用,并且支持代码的移动性。在此基础上提出了高阶Web服务和高阶服务组合的概念,并且给出了形式化描述和相关的架构。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论和相关研究
• 1.1 研究背景
• 1.2 服务组合的研究概要
• 1.2.1 服务组合的定义及研究内容
• 1.2.2 服务组合形式化方法的相关研究
• 1.2.2.1 模型验证
• 1.2.2.2 数理逻辑
• 1.2.2.3 自动机
• 1.2.2.4 Petri网
• 1.2.2.5 进程代数
• 1.2.3 主要的形式化方法比较
• 1.3 本研究的意义
• 1.4 本文研究内容
• 1.5 本文组织结构
• 1.6 本章参考文献
• 第二章 扩展的PI演算:P1-BEAM
• 2.1 语言
• 2.1.1 语法
• 2.1.1.1 带约束的通道束
• 2.1.1.2 逻辑并行链接和逻辑选择
• 2.1.2 规约语义
• 2.1.2.1 结构化同余
• 2.1.2.2 化简语义
• 2.1.2.3 LTS
• 2.1.3 类型系统
• 2.1.3.1 类型化
• 2.1.3.2 运行错误
• 2.2 合理性
• 2.2.1 类型系统的合理性
• 2.2.2 束通道的有界合理性
• 2.2.3 进程的束通道平衡合理性
• 2.3 等价性
• 2.4 图形化表示
• 2.4.1 相关图形化表示
• 2.4.2 标注连接进程图
• 2.5 PI演算的实验环境
• 2.5.1 实验环境整体结构
• 2.5.2 Pi演算编译执行环境
• 2.5.2.1 包结构图
• 2.5.2.2 编译器前端
• 2.5.2.3 编译器后端
• 2.6 小结
• 2.7 本章参考文献
• 第三章 基于PI-BEAM的服务组合验证
• 3.1 服务组合验证的研究内容
• 3.2 服务和服务组合表示
• 3.3 流程正确性
• 3.3.1 算法:基于流程正确性保证自动组合算法
• 3.4 类型相容验证
• 3.5 可达正确性验证
• 3.5.1 算法:接受可达性判定与求不可达节点集合的算法
• 3.6 活锁和活锁自由的验证
• 3.7 死锁和死锁自由的验证与避免
• 3.7.1 利用范式来判断死锁
• 3.7.2 利用进程的序类型来判断死锁
• 3.7.3 算法:利用进程的序类型来判断死锁的算法
• 3.7.4 利用进程的序类型来避免死锁
• 3.7.4.1 资源有序
• 3.7.4.2 打破wait-for圈
• 3.7.4.3 引入定时器控制
• 3.8 互模拟等价性验证
• 3.8.1 互模拟等价性检查在服务组合中的应用
• 3.8.2 算法:检测互模拟等价的算法
• 3.9 实验
• 3.10 小结
• 3.11 本章参考文献
• 第四章 QOS感知WEB服务组合的PI-BEAM-COST演算建模与模拟
• 4.1 问题描述
• 4.1.1 服务的QoS
• 4.1.2 QoS感知的服务组合问题
• 4.1.3 QoS感知的服务组合方法
• 4.1.4 基于进程代数的智能系统的形式化方法
• 4.2 语言
• 4.2.1 语法
• 4.2.2 语义
• 4.2.2.1 结构化同余
• 4.2.2.2 LTS
• 4.2.2.3 Cost测度操作符
• 4.2.2.4 等价服务的Cost测度
• 4.2.2.5 PSO的元控制过程
• 4.3 使用PSO的QoS感知WEB服务选择的建模与设计
• 4.3.1 场景
• 4.3.2 Pi-beam-cost来进行QoS感知的Web服务组合的原理
• 4.3.3 PSO的优化过程
• 4.3.4 DPSO模式的设计
• 4.3.4.1 DPSO介绍
• 4.3.4.2 解的表示
• 4.3.4.3 粒子的物理表示
• 4.3.4.4 粒子动力定义
• 4.3.4.5 Fitness函数的设计和计算
• 4.3.4.6 DPSO的主要过程
• 4.4 仿真模拟
• 4.4.1 仿真平台的建立
• 4.4.2 实验结果
• 4.5 小结
• 4.6 本章参考文献
• 第五章 高阶分布式PI演算的服务组合
• 5.1 研究背景
• 5.2 PI-BEAM演算的扩展:HOPI-BEAM
• 5.2.1 高阶扩展
• 5.2.2 分布式扩展
• 5.2.2.1 域
• 5.2.2.2 抽象进程的迁移应用
• 5.2.2.3 名字的复合表示
• 5.3 语言
• 5.3.1 语法
• 5.3.2 类型
• 5.3.3 语义
• 5.3.3.1 结构化同余
• 5.3.3.2 化简语义
• 5.4 高阶WEB服务和高阶WEB服务组合
• 5.4.1 高阶Web服务
• 5.4.2 高阶Web服务服务组合
• 5.4.3 高阶Web服务组件的WSDL表示
• 5.4.3.1 高阶Web服务组件
• 5.4.3.2 WSDL的高阶服务扩展
• 5.5 MAPREDUCE的框架的高阶服务视角研究
• 5.5.1 MapReduce简介
• 5.5.2 用高阶分布式Pi-beam演算来描述MapReduce框架
• 5.5.3 MapReduce作为高阶Web服务组合
• 5.6 MAPREDUCE服务模拟环境及实验
• 5.6.1 系统架构
• 5.6.2 WSDL的扩展与解析实现
• 5.6.3 代码的移动性
• 5.6.4 并发线程库的设计
• 5.6.5 模拟实验
• 5.7 小结
• 5.8 本章参考文献
• 第六章 总结和展望
• 符号表
• 缩略词表
• 致谢
• 攻读博士学位发表的论文
• 攻读学位期间参与的科研工作