UC San Diego

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 the state information updated as the interaction progresses, and receives user inputs. 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. My research establishes that under what conditions, automatic verification of such properties is possible, and reveals the complexity of verification. This brings into play a mix of techniques from logic to automatic verification. In addition, we also present WAVE, a verifier we implemented for interactive, database-driven Web applications specified using high-level modeling tools such as WebML, to demonstrate that our solution is indeed practically feasible. WAVE is a sound and complete verifier for a broad class of applications and temporal properties. Based on our experiments on four representative data-driven applications and a battery of common properties, WAVE yielded surprisingly good verification time, on the order of seconds. This suggests that interactive applications controlled by database queries may be unusually well suited to automatic verification. The experimental results 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 not only to the database area, but also to the automatic verification in general