document: Design for verification for asynchronously communicating Web services We present a design for verification approach to developing reliable web services . We focus on composite web services which consist of asynchronously communicating peers . Our goal is to automatically verify properties of interactions among such peers . We propose a design pattern that eases the development of such web services and enables a modular , assume-guarantee style verification strategy . In the proposed design pattern , each peer is associated with a behavioral interface description which specifies how that peer will interact with other peers . Using these peer interfaces we automatically generate BPEL specifications to publish for interoperability . Assuming that the participating peers behave according to their interfaces , we verify safety and liveness properties about the global behavior of the composite web service during behavior verification . During interface verification , we check that each peer implementation conforms to its interface . Using the modularity in the proposed design pattern , we are able to perform the interface verification of each peer and the behavior verification as separate steps . Our experiments show that , using this modular approach , one can automatically and efficiently verify web service implementations .
doc_bio_tags: 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 I I 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 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 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 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