基于Petri网的Web服务组合模型描述和验证

Petri-Net-Based Description and Verification of Web Services Composition Model

Web服务及其组合的形式化描述和验证是Web服务中一个重要的研究方向。分析了基于Petri网建模的优势,给出基于Petri网的Web服务的形式化定义和描述,对Web服务组合进行建模及元素映射,给出Petri网模型生成算法并对组合服务模型的可达性、安全性、有界性与活性等特性进行验证分析。最后是对一个具体的业务流程的建模和验证分析。由分析可知,该建模方法具有一定的表达和验证Web服务组合模型的能力。

Formal description and verification of web services and their composition are important research issues. The advantages were discussed for modeling web services composition using Petri net, Based on Petri net theory, the formal definition and graphic description were proposed for web services and their composition; the element mapping process was also illustrated. Then an algorithm was proposed to construct the Petri net model for web services composition. The reachability, safeness, boundness and liveness of the model were also validated. As an example, a concrete web services composition for a system was modeled and validated based on Petri net method, it showed that this modeling approach has enough capability in expressing and verifying web services composition.