The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

An Isaac Newton Institute Workshop

Logic and Databases

Automatic verification of communicating data-aware web services

28th February 2006

Author: Victor Vianu (UC San Diego/INRIA)


This talk presents recent work at UC San Diego on the verification of compositions of web service peers which interact asynchronously by exchanging messages. Each peer can be viewed as a data-aware reactive system. It 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. Finally, we present encouraging experimental results on verification of single peers (WAVE project). These suggest that automatic verification may be practically feasible for a large class of data-aware web services.

Related Links