面向服务计算(Service-Oriented Computing，SOC)代表着分布式计算和软件开发的最新发展方向。Web服务组合技术为Web服务的重用以及增值提供了解决方案，是SOC的核心技术之一。BPMN是首个为基于消息交互的松耦合系统集成建模而设计的业务过程建模语言，提供基于业务流程的Web服务组合方法，是目前应用在Web服务组合方面极为重要的标准。　　 基于BPMN的Web服务组合模型作为在分析时的交换依据，其语义正确性是服务组合能够得以实现、并以预期的方式工作的基础。但是，由于BPMN不是形式化的建模语言，结构比较自由且缺乏精确的语义，加上Web服务组合本身是一个复杂的过程，使得BPMN模型比一般的基于图形表示的流程更易于出现语义错误。BPMN模型的正确性需要在服务组合实施前得到保证。形式化方法是对系统进行分析的有效途径，对BPMN模型进行形式化分析具有重要的理论和实际意义。　　 本文通过应用形式化分析方法，采用COWS进程代数对BPMN模型进行形式化描述和分析，并结合性质的SocL，时态逻辑表示，给出BPMN模型的形式化验证过程。本文的主要工作有：　　 (1)分析基于BPMN的Web服务组合方法，通过对面向服务系统的形式化方法的研究，提出一套基于COWS的BPMN元素建模规则，定义了BPMN模型的精确语义。同时对COWS的语法和操作语义进行扩展，为复杂的Web服务处理过程赋予清晰形式化语义。　　 (2)对BPMN模型正确性分析，包括：对BPMN结构正确性，定义合理BPMN模型；使用COWS的操作语义推演理论来验证BPMN系统协作的正确性；分析组合服务系统的业务正确性，并用SocL时态逻辑进行形式化描述。　　 (3)在上述理论研究的基础上，设计实现了BPMN向COWS模型转换的自动转换工具，并结合使用CMC模型检测工具，对BPMN的COWS模型进行自动化验证。