Title:   Specification and Verification of Interactive, Data-Driven Web
         Applications
Speaker: Liying Sui (UCSD)

Abstract:

We study data-driven Web applications provided by Web sites
interacting with users or applications. The Web site can access an
underlying database, as well as state information updated as the
interaction progresses, and receives user input. The structure and
contents of Web pages, as well as the actions to be taken, are
determined dynamically by querying the underlying database as well as
the state and inputs. The properties to be verified concern the
sequences of events (inputs, states, and actions) resulting from the
interaction, and are expressed in linear or branching-time temporal
logics.

The results establish under what conditions automatic verification of
such properties is possible and provide the complexity of
verification. This brings into play a mix of techniques from logic and
automatic verification.

In addition, we also present WAVE, a verifier for interactive,
database-driven Web applications specified using high-level modeling
tools such as WebML.  WAVE is complete for a broad class of
applications and temporal properties. 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 can be
extremely effective. This is significant both to the database area and
to automatic verification in general.