面向服务架构(SOA)是先进的业务逻辑和计算理念,面向服务开发是对面向对象、面向过程及面向数据库开发的重要补充。面向服务开发的方法正在成为体现模块化,促进复杂的信息系统功能进行分配的最新技术解决方案。在SOA解决方案中,业务流程的建立不但是企业信息化战略的执行过程,而且是企业信息化系统的关键过程。因此,以研究服务组合语言为出发点,构建出良好的SOA流程,是很值得研究的课题。本文使用了一种流行的服务编制语言BPEL来实现业务流程。它通过组合、编排和协调Web服务,自上而下地实现面向服务的体系结构。BPEL语言有较强的表达能力,但BPEL结构上的复杂性会使其语义不是很清楚,所以在实际应用中对BPEL程序的正确性提出了很高的要求。为了更好的理解BPEL流程,需要采用形式化建模的方法对其流程进行建模。本文使用了一种简单的进程代数(FSP)的形式化方法对BPEL语义进行描述,并将一些简单的BPEL流程映射成LTS图。论文以并发进程共享资源问题为具体的研究对象,建立了其BPEL流程模型。然后,使用了一种适合于并行系统和协议一致性分析的模型检测工具SPIN,完成对形式化模型的验证。其中,本文实现了从BPEL流程到模型检测器SPIN的输入语言Promela之间的转换,并且成功的进行了验证；同时,本文对并发进程共享资源协议设计了其Kripke结构和LTL模型。分别的在模型检测器SPIN中将Kripke结构映射为Promela语言,将LTL公式嵌入到Promela程序中进行检验。从而讨论了支持编制的模拟和验证。最后,对本文所做工作进行了总结,并给出了后续工作的建议。