论文部分内容阅读
面向服务的体系架构(Service-Oriented Architecture,SOA)代表了分布式计算和软件开发的最新发展方向,Web服务作为SOA的实现方式之一,其价值在于服务重用,基于面向服务架构的Web服务组合技术为服务的重用以及增值提供了解决方案,它具有松散耦合、行业支持、高度可集成能力等优势。Web服务组合研究领域的一个重要的问题是如何形式化描述Web服务组合,如何验证服务组合的正确性。Web服务组合的形式化模型可以用来检查、验证Web服务组合以保证组合的正确性。Web服务组合涉及多个Web服务通信协作,这一特点使得Web服务组合的验证更加困难。而且,Web服务的组合语言作为一种基于业务流程的服务组合方法,建模理论基础比较薄弱,组合正确性的保证较弱。因此流程的正确性、无死锁性等问题,在它正式被实施前必须得到形式上的模拟与检验。本文针对上述问题,提出了一种基于Pi演算的Web服务组合的建模方法,利用Pi演算的并发计算操作符,将Web服务组合建模为一组并发执行的Web服务的组合,在此基础上验证Web服务组合流程的正确性。主要研究成果包括以下四个方面:(1)在对进程代数理论、Web服务组合建模以及BPEL4WS规范特性进行研究的基础上,系统地给出了从Web服务组合语言BPEL4WS规范到Pi演算的映射。(2)提出了一种基于Pi-演算的方法来形式化并且验证WS-CDL编舞。该方法可以保证WS-CDL编舞的正确性以降低由于Web服务执行的失败带来的开销。(3)对于用Pi演算形式化描述和建模的Web服务组合进行正确性的验证,对于验证后的Web服务组合给出反馈意见。(4)本课题用一个具体的交易场景验证WS-CDL模型设计的正确性。本文对Web服务组合流程的验证不是停留在架构层面上,而是直接对Web服务组合语言编写的程序代码进行验证,因此更具有可行性和实用性。