Formal description and verification of web service composition based on OOPN

Abstract

To overcome the shortcomings of unable to demonstrate the characteristics of encapsulation, reusability and message-driven when using Petri nets to model Web service composition, this paper proposes object oriented Petri nets (OOPN) as the formal description and verification tool for Web service composition. Some basic concepts of OOPN, including class net, inheritance, object net and object net system, are given in the paper respectively and the mechanisms of "Gate" and "Port" are used to describe message transfer and synchronization relationships among objects. The OOPN expressions of various basic control flow structure and message synchronization relationships of Web service composition are also stated. Finally, we give a case study to show that our proposed method can more naturally and accurately demonstrate the encapsulation and message-driven characteristics of Web services. © 2008 Springer-Verlag Berlin Heidelberg.