Verification of Communicating Data-Driven Web Services
Skip to main content
Open Access Publications from the University of California

Verification of Communicating Data-Driven Web Services


We study the verification of compositions of Web Service peers which interact asynchronously by exchanging messages. Each peer has access to a local database and reacts to user input and incoming messages by performing various actions and sending messages. The reaction is described by queries over the database, internal state, user input and received messages. We consider two formalisms for specification of correctness properties of compositions, namely Linear Temporal First-Order Logic and Conversation Protocols. For both formalisms, we map the boundaries of verification decidability, showing that they include expressive classes of compositions and properties. We also address modular verification, in which the correctness of a composition is predicated on the properties of its environment.

Pre-2018 CSE ID: CS2006-0853

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View