Verifying web services composition based on hierarchical colored petri nets

Current Web services composition proposals, such as BPML, BPEL, WSCI, and OWL-S, provide notations for describing the control and data flows in Web service collaborations. However, such proposals remain at the descriptive level, without providing any kind of mechanisms or tool support for verifying the composition specified in the proposed notations. In this paper, we present to verify Web services composition by using CP-nets. CPnets combine the strengths of Petri nets with the expressive power of high-level programming and have sound mathematical semantics. These services composition proposals can be transformed by transformation rules into CP-nets, which can be used to analyze the performance and to investigate behavioral properties such as deadlock or livelock by CP-nets tools. Categories and Subject Descriptors .D.2.4 [Software Engineering]: Software/Program Verification – Formal methods, Reliability, Validation. General Terms Reliability, Experimentation, Languages, Verificati...

• Type: Conference
• Year: 2005
• Where: IHIS
• Authors: Yanping Yang, QingPing Tan, Yong Xiao
• Keywords: IHIS 2005, Information System, Services Composition, Services Composition Proposals, Web Service