Web服务是各种商业、应用、系统服务的基于XML标准的接口。以其开放性、标准性 和简便性而得到了迅速的推广，改变了基于Internet应用程序的开发方式。Web服务组合是 一个分布式的开发架构，以现存的Web服务为基础去建构出一个新的Web服务。通过Web 服务组合的应用将可以实现具备更多功能更有价值的企业流程。 BPEL是一种基于工作流的Web服务组合语言。它用XML描述如何把Web服务组合成 一个商业流程，并且把流程本身描述成一个新的Web服务。然而，由于BPEL本身的复杂 性，BPEL的实施和部署有一定的难度。开发者所设计出来的Web服务流程很有可能会产生 死锁、不可达等问题。这些问题往往无法从表面的设计进行判断，因此必须通过建模工具的 运用，才能分析和验证流程的运行状态从而发现死锁、可达性和安全性等问题。 BPEL流程从设计开发到部署实施是一个复杂的过程，设计过程出现的任何错误都会对 商业应用带来难以估计的损失。如何保证BPEL流程在设计阶段就满足正确性的要求，成为 一个亟待解决的问题。目前还没有BPEL流程的开发设计软件可以做到以Petri网理论为基 础的流程实时分析验证，在理论上给予流程设计以正确性保证。 如今已成热点的企业应用集成(EAI)项目中，业务流程整合更是其不可或缺的部分。 企业的业务流程会同时涉及到多个应用系统，因此要求这些系统能够协同工作。但是接口、 架构的不统一往往使得这些本应紧密集成的应用系统成为了一个个“信息孤岛”。如何抽象底 层应用的逻辑和消息组件，允许业务用户创建跨越多个系统的复杂流程成为解决此类问题的 关键所在。 本文在对现有形式化方法分析的基础上，根据Web服务体系结构的特点，综合应用Petri 网、工作流等分析技术，提出并研究了用于Web服务流程组合语言BPEL的性质分析的Web 服务工作流网BPWS-Net和正确性验证准则。设计并实现了一个Web服务流程开发与验证 系统。提出一个基于XML的远程服务架构(RS-Link)的设计与实现方案。 综上所述，本文工作的主要贡献表现在如下几个方面： (1)提出了面向服务的Web服务工作流网BPWS-Net。与现有的BPEL流程建模方法 相比，BPWS-Net能够更加全面、具体的反映BPEL的语言特性。BPWS-Net不仅对BPEL 中的基本活动、结构化活动给出了确切的形式化定义，并且对BPEL的链接语义、死路删除、 异常处理等特性做了形式化描述。BPWS-Net中各子网的继承关系，能够准确的反映BPEL 中的活动嵌套关系，便于对流程进行分层描述与建模分析。 (2)提出了BPWS-Net的正确性验证准则。利用Petri网的形式化分析技术，定义了 BPWS-Net的安全性、可达性和无死锁性，以及BPWS-Net的正确性验证方法。 (3)设计并实现了一个基于BPWS-Net的BPEL流程开发与验证系统。验证系统可以 在BPEL流程设计过程中，自动生成对应的BPWS-Net模型和可达树(图)，利用BPWS-Net 的正确性验证方法判定流程的正确性。与其他的BPEL流程开发系统相比，本系统将Petri 网的形式化分析技术应用到流程开发过程中，减小了BPEL流程出错的可能性，缩短了开发 与测试周期。 (4)在BPEL流程开发与验证系统中，本文对BPWS4J的功能进行了扩展，使得BPWS4J 引擎可以处理复杂数据类型，以满足企业级应用的要求。并设计开发了流程日志监控平台， 可以增强BPEL状态查询方面的不足，使得分布式环境下的流程监控成为可能。 (5)提出了一个基于XML的远程服务架构(RS-Link Framework)，并给出了详细的设 计与实现说明。RS-Link是在Web服务、BPEL等开放标准的环境下，对ERP、SCM、Web 服务、网格服务等异构系统进行整合的底层框架。是一个通用的、灵活的、可扩展的基础框 架软件，为系统架构提供统一的访问接口，以满足系统之间无缝共享和交换数据的需要。利 用BPEL流程开发与验证系统，可以有效地对异构系统所组成的Web服务流程进行建模分 析与验证。 关键词：Web服务，BPEL，Petri网，工作流，建模，EAI