Web服务的出现代表了分布式计算的新要求,较好地解决了异构应用之间及松散耦合环境下的互操作和集成问题。随着Web服务的发展与应用,Web服务组合技术成为Web服务研究的关键问题。业务流程执行语言(Business Process Execution Language,BPEL)作为执行过程定义的标准,由于商业逻辑的复杂性,使用BPEL流程组合Web服务容易出错,因此,需要采用有效的方法来建模、分析、验证BPEL流程,从而保证业务流程的正确高效运行。本文在同步Petri网的基础上引入了一些有色Petri的概念,针对BPEL的特点,在不改变同步Petri网的基本性质的前提下对同步Petri网作了一些扩展,提出了一种更适合BPEL建模的SPN-NET模型。该模型简洁紧凑,可理解性好。同时给出了BPEL与SPN-NET模型的转换规则,并给出了相互转换的算法。为了进一步简化模型,提出了一种基于结构相似性的化简算法。文中给出了基于SPN-NET模型的服务组合合理性验证和性能分析方法。在合理性验证上,利用已有的化简规则并且扩展了2个规则进行化简来验证BPEL流程的结构合理性,同时在普通Petri网可达图的基础上给出了此模型的可达图合理性分析方法。在性能评估上,结合马尔可夫链方法,详细给出了排队论和等价化简方法相结合的性能评估方法。最后,设计了基于SPN-NET建模工具的总体框架,并结合开源系统[fireworkflow],初步实现了基于SPN-NET的建模工具。文中给出了模型的动态描述,完成了几个结构性BPEL流程文档向SPN-NET的转换示例,并且给出了测试结果,最后结合实例对流程进行了单步动态模拟。本文主要是对基于工作流的Web服务组合建模进行了相关研究,提出了一个更适合BPEL建模的模型SPN-NET,基本上解决了建模技术中的主要问题,对于推进基于工作流Web服务组合技术的研究具有一定的价值。