Modeling and Verification of Session-Oriented Interactions between Web Services: Compliance of BPEL with Session Protocols

Abstract

Although web services are generally envisioned as being stateless software systems, some of them are implicitly stateful. The reason is that the web services often work as front-ends to enterprise systems and are used in a session-oriented way by the clients.

Contrary to the case of stateless services, for a stateful web service there exist constraints to the order in which the operations of the service may be invoked. However, specification of such constraints is not a standard part of a web service interface, and compliance with such constraints is not checked by the standard web service development tools.

Therefore, we propose in this paper to extend a web service interface by a constraint definition that is based on behavior protocols. Also, we implemented a tool that checks whether a given BPEL code complies with the constraints of all stateful web services it communicates with.

The key idea behind the tool is to translate the BPEL code into a Java program and then to check the Java program using Java PathFinder with a behavior protocol extension.