Home // SERVICE COMPUTATION 2014, The Sixth International Conferences on Advanced Service Computing // View article

Analyzing Behavioral Compatibility for Web Service Choreography Using Colored Petri Nets and ASK-CTL

Authors:
Maya Souilah Benabdelhafid
Béatrice Bérard
Mahmoud Boufaida

Keywords: Web Service Choreography; Behavioral Compatibility; Model Checking; CPN; ASK-CTL

Abstract:
Web services have become the technology of choice for Service-Oriented Computing (SOC) implementation. Their composition is a recent field that has seen a flurry of different approaches proposed towards the goal of flexible distributed heterogeneous inter-operation of software systems. These systems are usually derived from higher-level models rather than be coded at low level. In practice, achieving Web service compatibility nonetheless continues to require significant efforts for modeling at multiple abstraction levels. Existing formal approaches typically require the analysis of the global space of joint executions of interacting Web services. We propose a formal approach where Web service choreography is represented with the high-level model of Colored Petri Nets (CPNs). ASK-Computational Tree Logic (ASK-CTL) is used to describe the behavioral compatibility of these services in terms of message order properties. Then, model checking is applied for the verification of these properties. The effectiveness of our work has been validated with the recent version of CPN Tools.

Pages: 32 to 39

Copyright: Copyright (c) IARIA, 2014

Publication date: May 25, 2014

Published in: conference

ISSN: 2308-3549

ISBN: 978-1-61208-337-7

Location: Venice, Italy

Dates: from May 25, 2014 to May 29, 2014