The goal of this project is the Specification and Verification of Interactive Web Applications powered by an underlying database. The project allows web application designers to declaratively specify the behavior of an interactive web application as a function of the user input, the current state of the application, and the information in an underlying database.
Desirable properties of the web application can be specified and verified statically, at design time.
WAVE is a tool implemented in Java for verifying temporal properties of data-driven Web applications. WAVE takes as inputs the specification of a Web application (written in a declarative, rule-based specification language) and a property (expressed in first-order temporal logic), and outputs whether the property is true or false for that Web application together with plenty of useful verification information (such as a counterexample in case of a false property).
Interactive web applications have emerged as a major paradigm for publishing information on the Internet. These applications are increasingly complex, requiring static analysis tools for boosting the confidence in their robustness and correctness and for enhancing their functionality and efficiency.
This demo illustrates our framework for web application specification. In the future, the demo will be extended to illustrate the automatic generation of web applications from specifications, and the verification of properties.