Paper Title: Analyzing Web Service Choreography Specifications Using Colored Petri Nets
Enacting cross-organizational business processes requires critical support for long-running and complex interactions involving multiple participants. The Web Services Choreography Description Language (WS-CDL) aims at facilitating just that, by providing means to describe correlated message exchanges among services geared towards achieving a business goal. While WS-CDL specifications are machine-readable documents, they do not necessarily allow developers to determine—by direct inspection—whether or not the patterns of message exchanges they stipulate do indeed describe the intended service behavior. In this research paper, we show how Colored Petri Nets (CPN) can be used to analyze WS-CDL documents in order to identify faults in the specification. We have developed a research prototype that assists in the creation of a CPN model from a given WS-CDL document. The CPN model generated is then analyzed using the formal verification environment and simulation capability provided by CPN-Tools. We provide a discussion on the analysis of an example WS-CDL document using this approach, as well as on the advantages and limitations of using CPN for analyzing WS-CDL specifications.
Authors: Enrique Caliz, Karthikeyan Umapathy, Arturo J. Sánchez-Ruíz, and Sherif A. Elfayoumy
Conference Link: http://www.desrist2011.uwm.edu/