document: 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 checker is a finite-state verification tool we can only achieve partial verification by fixing the sizes of the input queues in the translation . We propose the concept of synchronizability to address this problem . We show that if a composite web service is synchronizable , then its conversation set remains same when asynchronous communication is replaced with synchronous communication . We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically . Based on our synchronizability results , we show that a large class of composite web services with unbounded input queues can be completely verified using a finite state model checker such as SPIN .
doc_bio_tags: O O O B O O O O O O O O O O O O O O O O O O O O O O B O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B O O O O O O O O O O O O O O O O O O O O O O O O O B O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B O O O O O O O O O O O O O O O O O B O O B O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B O O O O O O O O O O O B I O O O O O B O O O O B I O O O O O O O O O O O O O O O B O O O O O O O O O O B O O O O O O O O O O O O O O O O O O O O O O O O O O O O B O