Modern Web applications are often powered by an underlying database and
generate their pages dynamically as a function of internal state,
database contents, as well as the user's actions (e.g. clicking on a
button/link, selecting an item from a menu, inputing text, etc.). The
resulting user interaction is governed by a workflow of considerable
complexity, with high bug potential, which is usually realized. To boost
both the developers' and users' confidence in the correct behavior of
the Web application, we developed WAVE, an automatic design-time
verifier for interactive, database-driven Web applications specified
using high-level modeling tools such as WebML.

WAVE allows the developer to specify desired properties of the temporal
evolution of the interaction with the user (aka "runs"). For instance,
"regardless of  what the user does and regardless of the database
contents, book orders will be placed only if the correct payment is
received". WAVE is a sound and complete verifier for a large class of
properties and applications, i.e. it declares an application correct if
and only if for every database contents, every corresponding run
satisfies the properties. A counterexample database and run are
exhibited otherwise. For other applications, WAVE can be used as an
incomplete verifier, as commonly done in software verification. Our
experiments on four representative data-driven applications and a
battery of common properties yielded surprisingly good verification
times, on the order of seconds. This suggests that interactive
applications controlled by database queries may be unusually well suited
to automatic verification. They also show that the coupling of model
checking with database optimization techniques used in the
implementation of WAVE is extremely effective. These findings are
significant both to the database area and to automatic verification in
general.

This is joint work with Victor Vianu, Liying Sui and Dayou Zhou, all
from UCSD.


The talk assumes no prior model checking background.