论文部分内容阅读
随着Web服务技术的研究、发展和应用，众多学者试图寻找Web服务组合验证的有效方法，开始运用形式化方法描述Web服务组合并对其进行分析。目前国内外有使用进程代数、petri网、spin等工具来形式化建模、验证Web服务组合语言，但是他们都存在某些不足，而且多限于探索或者仅停留在理论研究阶段。
本文在对现有Web服务形式化验证方法的研究基础上，讨论了它们的特点和不足，并详细分析了现在广泛使用的Web服务组合语言标准BPEL4WS规范的特性，提出了一套基于pi演算的BPEL4WS的建模规则，之后深入研究了类型系统理论，提出了一种切实可行的基于类型化pi演算的Web服务组合相容性分析方法。
本文的研究内容主要包括三部分：第一部分是对BPEL4WS规范形式化建模的研究，对pi演算进行了顺序算子的扩充，给出了扩充的语法和操作语义，并用pi演算的通信并发结构表示BPEL4WS规范的link结构；基于对BPEL4WS规范死路排除DPE模式的分析，提出了一个完善的解决DPE问题的pi演算形式化方法，从而系统地完成了从Web服务组合语言BPEL4WS规范到扩充pi演算的映射；第二部分是对类型系统的研究，我们区分了通道的输入输出能力，将类型互模拟关系扩充到了区分传输能力的通道类型上，并给出了相关性质和定理的证明；我们给出了类型互模拟和子类型的关系，重新定义了类型上下文环境，给出了进程类型定义良好的推理规则，最后定义了类型化pi演算的规约语义。第三部分在前面两部分研究的基础上，用类型化pi演算对BPEL4WS描述的Web服务组合系统做了形式化表示，提出了基于类型化pi演算的服务组合相容性检测算法，最后给出了一个银行贷款审批系统的完整检测实例，说明利用该算法检测服务组合系统相容性的可行性。