浅谈基于Petri网的Web服务组合建模与验证

　　摘要：该文首先提出了基于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服务的唯一标识。
　　2） SName为Web服务的名称。
　　3） SDesc为Web服务的描述。
　　4） URL为服务的调用地址。
　　6） PN为Web服务的Petri网。
　　1.3 服务的组合结构
　　Web服务组合的组件由原子服务和合成操作组合而成。其中，此处原子服务可能是基本服务，也可能是组合服务。基本的组合操作有顺序，选择，循环，并行，调用这五种类型，这些组合操作可以由基本服务组合而成，其他更复杂的服务组合操作可以由这些基本的组合结构组合而成。基本服务的Petri网结构如下，其中i，o分别表示服务的输入和输出库所，s表示服务的操作。
　　给Web服务建模以后，接下来就可以应用Petri网的分析方法来进行验证分析。
　　2 Web服务组合的验证
　　Petri网提供了许多强大的分析工具，，如可达树分析、可达图分析、马尔可夫分析、关联矩阵与状态方程、Petri网语言等。其中，可达树是用来描述所有从初始状态开始的可达状态。在可达树中，M0代表树的根结点，叶子结点代表系统的最终状态，弧代表相关的转换。从根结点到一个确定的结点的路径代表一个可执行的序列。该文采用可达树作为分析工具。通过对Petri网的性质进行验证，可以验证组合服务的正确性。具体的可达树构造算法这里不再列出，详见文献[7]。Petri网的主要性质有：
　　3 Web服务组合的验证实例分析
　　某公司员工要到外地出差，由于目的地距离公司所在地较远，该员工打算乘坐高铁或者飞机去往目的地。首先该员工要通过火车票查由上述分析可知，该服务组合模型是合理的，满足正确性的要求。
　　4 结束语
　　本文提出了一种基于Petri网对组合服务进行建模的方法，给出了Web服务的形式化定义，并给出了图形化表示，最后结合具体的实例来进行建模分析，并采用可达树作为分析工具来验证组合服务的正确性。Petri网提供了一种有效的手段去模拟、分析和验证Web服务组合，然而，在建立许多大型、复杂的系统模型时，Petri网也表现出了一些明显的不足。 所以，如何在建立复杂Petri网模型时，尽量降低其复杂度是接下来的主要研究工作。