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

摘要

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.