Web服务是一种面向服务架构的技术,通过标准的Web协议提供服务,目的是保证不同平台的应用服务可以互操作。它具有自包含、自描述、模块化特点,因此,Web服务是构造开发分布式系统的基础模块,它们允许所有的企业和个人快速、廉价建立和部署全球性的应用。Web服务组合可以把多个由WSDL定义的无状态的Web服务组合成有状态的业务流程,满足多变的业务需求。在满足功能需求的前提下,组合服务的性能是赢得用户的关键,可部署一个的试验床系统来评价Web服务组合系统的性能,代价是昂贵的且耗时的。因此,Web服务组合的性能建模是Web服务组合的再工程中重要的研究方向。目前,大多数对Web服务组合的性能建模的研究主要是基于数学分析的方法来分析服务组合的性能,然而这样分析的前提必须简化Web服务组合的执行环境,否则难以用数学的分析方法进行分析,这是因为Web服务组合的执行环境中可能包含了异常处理和补偿机制。因此,本文主要针对这样的问题,用形式化的方法研究了Web服务组合的性能建模和分析的问题,特别是对Web服务组合的异常处理和补偿机制进行了建模,并分别构建性能的仿真模型和数学分析模型。本文主要从以下内容来展开进行论述的。首先针对本文的研究重点BPEL业务流程,本文讨论了它的抽象语法和语义,认为BPEL业务流程需要用分为两个部分来构建性能模型,第一个部分是BPEL的基本控制流建模,第二部分是建模BPEL执行上下文,即对由于BPEL的异常处理和补偿机制所导致的控制流。本文讨论了BPEL所定义的复合Web服务在执行过程中可能出现的状态,在这个基础上提出了一种复合Web服务正常状态框架模型。然后,本文讨论了广义随机Petri网的建模能力。除了讨论通常的基本控制流构件构建方法外,如AND-split, OR-split, AND-join和OR-join结构,本文还特别利用在广义随机Petri网中变迁的定义,提出了一个能建模中断事件的重要结构,利用该结构能够近似地模拟BPEL的异常处理和事务处理的行为。同时,根据BPEL的基本控制流,本文在复合Web服务正常状态框架模型下提出了一种基于Petri网的服务组合代数方法,用于建模BPEL的基本控制流和复合Web服务组合的过程。为更好地支持长事务(Long-running Transaction)处理,BPEL提供了特殊的异常处理和补偿机制。本文研究了BPEL在执行过程中活动(复合Web服务)可能出现的状态,提出一种完全的复合Web服务状态框架,在该框架下讨论分析各类活动的状态空间模型和各个状态变化之间的关系,提出了一种使用状态变迁系统形式化建模复合Web服务状态空间模型的方法。最后,本文提出了WS-BPEL到广义随机Petri网映射方法,在此基础上对一个应用场景的BPEL流程进行了性能仿真和分析。