Web服务已经日渐成为一个重要的研究领域,学术界和工业界都对其非常关注.为确保多个Web服务能成功地协同完成一项复杂的工作,人们正越来越重视服务编排的概念,即从全局观点描述一个业务流程的多个参与方的行为和协作,从而实现某个共同业务目标的过程。WS-CDL是由W3C制定的用于描述Web服务编排的语言,但不少研究者指出,WS-CDL语言还相当不成熟,仍有很多问题尚未解决.形式化方法已被用于对基于消息通讯的并发系统进行建模和分析,进而认识并发系统、提高并发系统的正确性和可靠性.将形式化方法应用于Web服务领域已经成为一个重要的研究方向。本文研究了Web服务编排的演算,特别设计了一个作为Web服务编排的轻量级演算,给出了它的语义,并定义了基于编排的实现模型,建立了从编排到实现的投影,从而确保编排规范通过投影后得到正确的实现。这些研究可以帮助我们深入理解作为Web服务和应用基础的“编排”与“协作”的概念,弄清其基本属性和规律性,并进一步认识编排语言的设计与实现等方面的问题。本文的研究成果主要包括以下两个方面:1.Web服务编排的演算模型定义了演算模型的语法和语义:在语法上,通过使用一组算子构造角色进程之间的“交互”活动,其中包括不会死锁的消息通信活动R(?)~cR;语义上,考虑到编排是不可执行的抽象规范,因而使用迹语义,强调同步通信,对于并行复合活动,则采用交错运算。基于该轻量级演算模型诱导出了结构同余关系,包括预期的选择、顺序复合和并行复合的结构律,并证明了编排的无死锁特性.2.Web服务编排的投影实现受Orc的启发,把Orc面向服务的特点和π-演算的传名通信机制组合在一起,定义了Orc_π演算作为编排的实现模型.提出了投影projection的概念,建立了从编排演算到Orc_π演算的投影Pr_π,并给出了两个关于编排的可实现性语法条件及其证明系统。在此基础上扩展了Web服务编排的演算模型及其投影规则,并通过实例说明了投影实现的正确性.上述结果具有重要的理论和实际意义.通过这方面的深入理论研究,可以帮助我们进一步理解Web服务的本质和问题,为Web服务领域的发展奠定坚实的基础.同时,理论研究取得的成果也具有潜在的应用价值,能为新型的Web服务开发工具提供技术和方法.