丁冲冲++李婷婷

摘要：该文首先提出了基于Petri网的Web服务组合建模方法，对服务组合进行形式化建模，然后采用可达树作为分析工具，对服务组合模型的可达性，活性，有界性等特性进行验证分析。最后通过一个具体的实例说明此方法的应用。

关键词：Web服务；Petri网；可达树；Web服务组合；验证

中图分类号：TP311 文献标识码：A 文章编号：1009-3044（2014）15-3509-03

Web Services Composition Modeling and Verification Based on Petri Net

DING Chong-chong， LI Ting-ting

（College of Information Engineering， Nanjing University of Finance and Economics， Nanjing 210046， China）

Abstract： This paper first puts forward Web services composition modeling method based on Petri net. The formal modeling for Web services composition is also the article research content. Then the paper uses the reachability tree as the analytical tool to analyse and verify the features of services composition model， such as accessibility， activity and boundedness. Finally， the article uses a specific example to illustrate the application of this method.

Key words： Web services； Petri net； reachability tree； Web services composition； verification

基于Petri网的形式化建模方法是Web服务组合建模的一种重要的手段。Petri网是一种基于状态的建模方法，具有直观的图形表示，形式化语义定义，丰富的分析技术等优点。同时，由于Web服务的独立性和自治性，通过多个Web服务组合完成的业务流程的正确性难以保证，因此必须要对服务组合进行验证。基于Petri网的许多优点，该文利用可达树作为分析工具，对服务组合模型的可达性，活性，有界性等特性进行验证分析，进而验证服务组合模型的正确性。

1 基于Petri网的Web服务组合

1.1 Petri网的定义

2） T为变迁结点集合，代表引起系统状态改变的事件。

3） W为库所结点和变迁结点之间的有向弧集合，即流关系。

4） M0 为PN的初始标识。

5） i为输入库所，即i=φ。

6） o为输出库所，即o=φ。

1.2 Web服务组合的Petri网模型

由于Web服务在行为上是操作的偏序集，所以可以直接将Web服务映射到Petri网上。

服务的操作对应于变迁元素，服务的状态对应于库所，其中，Web服务的状态有五种，分别为“未实例化”、“就绪”、“执行”、“暂停”、“完成”。操作与状态之间的因果关系则作为变迁与库所之间的流关系。基于Petri网，Web服务被定义为一个六元组，S=（Id，SName，SDesc，URL，CS，PN），其中：

1） Id为Web服务的唯一标识。……