WAVE: Automatic Verification of Data-Driven Web Services

Data-driven Web services, viewed broadly as interactive sy stems available on the Web for users and programs, provide the backbone for increasingly complex We b applications. While this yields ever- increasing functionality, the added complexity renders su ch applications more vulnerable to bugs and failures, potentially compromising their robustness and c orrectness. Therefore, there is a need to develop verification techniques for such Web services. The WAVE project at UC San Diego aims to develop new approaches for automatic verification of data-driven We b services. The work relies on a novel, highly effective marriage of model checking and database te chniques. We summarize briefly the main contributions of the project, which range from theoreticalfoundations to the successful implementation of a prototype verifier.