A rewriting logic approach to the formal specification and verification of web applications

• Web-TLR is a verification framework for Web applications based on rewriting logic.
• Critical properties of Web applications can be efficiently model-checked in Web-TLR, e.g., security policies.
• A slice-based optimization allows the model-checking counter-examples to be drastically reduced.
• A graphical representation allows the counter-examples to be analyzed and debugged.

This paper develops a Rewriting Logic framework for the automatic specification and verification of Web applications that considers the critical aspects of concurrent Web interactions, browser navigation features (e.g., forward/back-ward navigation, page refresh, and new window/tab opening), and Web script evaluation. By encompassing the main features of the most popular Web scripting languages (e.g., PHP, ASP, and Java Servlets), our scripting language is powerful enough to model the dynamics of complex Web applications, where the interactions among Web servers and Web browsers are formalized through a landmark communicating protocol that abstracts HTTP. We provide a detailed characterization of browser actions via rewrite rules and show how our models can be naturally model-checked by using the Linear Temporal Logic of Rewriting (LTLR), which is a Linear Temporal Logic that is specifically designed for model-checking rewrite theories. The framework has been completely implemented in Maude, and we report on some successful experiments that we conducted using the Maude LTLR model-checker.