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 d...

• Type: Conference
• Year: 2005
• Where: WWW
• Authors: Aysu Betin-Can, Tevfik Bultan, Xiang Fu
• Keywords: Behavior Verification, Interface Verification, Internet Technology, Style Verification Strategy, WWW 2005