"Automated Verification and Testing of Legacy Web Applications Using WAVE"
 
Our prior work has established the WAVE framework for specification and 
verification of Web applications.  The paradigm proposed is one in which 
the Web application implementation is automatically generated from a verified 
specification.  In this work, we look at a different paradigm where the 
implementation already exists and did not necessarily come from a WAVE spec.  
Given a legacy Web application, we would like to verify its correctness and 
to be able to identify errors in its implementation.  Towards this goal, we 
propose a novel approach based on the WAVE framework.  This approach utilizes 
the high-level specification mechanism and verification power given by the 
WAVE framework, and extends the verification results to produce specialized 
programs for testing the Web application (known as Web test cases).  We have 
implemented WAVE-TC, an extension of WAVE with test case generation, and have 
obtained some preliminary experimental results.
 
This presentation will be self-contained and will require no prior knowledge
 of WAVE.