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.
- http://www.cs.ucsd.edu/users/lsui/project/index.html - Home page of WAVE project