Analysis of interacting BPEL web services

This paper presents a set of tools and techniques for analyzing interactions of composite web services which are specified in BPEL and communicate through asynchronous XML messages. We model the interactions of composite web services as conversations, the global sequence of messages exchanged by the web services. As opposed to earlier work, our tool-set handles rich data manipulation via XPath expressions. This allows us to verify designs at a more detailed level and check properties about message content. We present a framework where BPEL specifications of web services are translated to an intermediate representation, followed by the translation of the intermediate representation to a verification language. As an intermediate representation we use guarded automata augmented with unbounded queues for incoming messages, where the guards are expressed as XPath expressions. As the target verification language we use Promela, input language of the model checker SPIN. Since SPIN model chec...

• Type: Conference
• Year: 2004
• Where: WWW
• Authors: Xiang Fu, Tevfik Bultan, Jianwen Su
• Keywords: Composite Web Services, Internet Technology, SPIN Model Checker, Unbounded Input Queues, WWW 2004