论文部分内容阅读
Web服务组装作为一种跨组织业务流程的实现形式，得到了广泛的关注。通过把多个功能单一的Web服务集成到一起，可以提供实现复杂业务逻辑的完整解决方案。WS-BPEL（Web Service Business Process Execution Lnguage）是一种被广泛接受的、描述Web服务静态组装的语言。为了保证WS-BPEL描述的Web服务组装的可靠性，避免在实施过程中出现不必要的错误，需要在设计阶段、部署之前对其进行分析和验证，从而确保组装流程能够正确进行。
形式化方法是对系统建模和验证的一种重要的方法，在这方面已经做了许多工作并取得了重要的成果。一般的做法是：先对WS-BPEL流程建立具有精确语义的形式化模型，描述有关Web服务组装的某些性质，然后对这些性质进行分析和验证。然而已有的模型大多关注于WS-BPEL流程的某一方面，如控制流、语义描述、数据依赖关系等，对于WS-BPEL流程进行全面的、整体的建模和分析工作尚显不足。
针对上述问题，本文提出了对WS-BPEL流程进行层次化建模和分析的方法，在统一框架下，分别对底层的控制流和高层的数据流建模，并加以完善，使得所描述的内容更丰富，可以分析更多的性质，同时也降低了模型的复杂度。
本文采用同步网（一种Petri网）来描述除“死路删除”语义之外的WS-BPEL流程的控制流，把流程中的基本活动、各种结构化的活动以及表示并发活动之间控制依赖关系的链接都映射到该同步网的模型中，并给出了包括畅通性等性质的分析方法。为了描述活动间的时态逻辑关系，设计了从同步网到用Promela语言所描述模型的自动转换算法，从而能够使用模型验证工具SPIN实现对系统逻辑性质的自动验证。
死路删除是WS-BPEL流程中特有的操作，用于处理并发结构中活动同步时出现的连接错误。为了描述WS-BPEL中的死路删除的语义，本文建立了语义模型DPE网（Dead-Path-Eliminaltion Net）。该模型以token的颜色标记活动的执行状态和链接状态，并为每个变迁绑定一个条件表达式，以便于判断活动的执行方式。与使用P/T网得到的模型相比，引入颜色集和变迁可以降低DPE网的规模。对于包含较多链接的流程，此种方法带来的好处更突出。
WS-BPEL流程中数据流包括隐式数据流和显式数据流。本文利用有色网描述语言CPN ML为WS-BPEL流程中的活动建立了数据流模型，该模型支持对XML Schema类型数据的描述，并在此基础上讨论了一些与数据相关的性质的验证方法。
总之，本文采用控制流、数据流分层的方式，使用不同的Petri网对基于WS-BPEL的Web服务组装流程进行统一建模和分析，主要有WS-BPEL流程控制流的同步网模型、死路删除的语义网模型以及数据和消息流的有色网模型，分析和验证了WS-BPEL流程的链接性质、死路删除语义下的活动间关系以及其他与数据相关的性质。这一系列建模和分析过程，能够有助于设计人员更好地理解流程，发现流程中潜在的错误，提高 Web服务组装的正确性。