Web服务是一种新型的软件泛型，它具备松耦合、高动态性和可重配置等特点。Web服务组合通过为成员服务制定工作流程来实现具备复杂业务处理能力的组合服务，同时满足了用户不断变化的需求。此外，Web服务依靠其良好的可复用性和灵活性等特征，加上服务组合可实现增值服务的能力，使得面向服务的计算成为一种具有里程碑意义的分布式计算技术。　　 由于服务纲合为Web服务带来了增值和复用的优势，如何对Web服务组合进行建模、分析与验证，确保组合服务的质量与安全便成为一项值得深入研究的课题。现有的服务组合的验证方法一般从组合服务整体的状态或各成员服务之间的消息交互方面出发进行建模和分析；而本文则提出了一种扩展的控制流图(eXtended Control Flow Graph，XCFG)米对BPEL规范制定的组合服务工作流程进行建模，定义了XCFG的形式化描述，并在此基础上实现了BPEL中并发结构相关的属性：无死锁性、无冲突性和link无冗余性的分析及验证。　　 XCFG针对传统的控制流图进行了相应的扩展，使得其形式化模型能够满足对BPEL规范中提供的顺序、选择、并发和同步四种控制依赖关系进行描述。此外，在XCFG的每个活动节点元素中增加了对变量访问信息的记录，用来实现并发访问冲突的分析。理论和实验分析表明，通过XCFG能够有效的对BPEL规范制定的组合服务工作流程进行控制流的建模、分析和验证。同时，以XCFG为基础开发的自动化验证工具XCFGV4BPEL实现了从BPEL文档解析生成相应的BPEL对象模型(BPELObject Model，BOM)、BOM至XCFG的映射到基于XCFG进行并发结构相关属性的形式化分析与验证的完整解决方案。