Specification and Verification of Web Applications in Rewriting Logic

Abstract. This paper presents a Rewriting Logic framework that formalizes the interactions between Web servers and Web browsers through icating protocol abstracting HTTP. The proposed framework includes a scripting language that is powerful enough to model the dynamics of complex Web applications by encompassing the main features of the most popular Web scripting languages (e.g. PHP, ASP, Java Servlets). We also provide a detailed characterization of browser actions (e.g. forward/backward navigation, page refresh, and new window/tab openings) 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 specifically designed for model-checking rewrite theories. Our formalization is particularly suitable for verification purposes, since it allows one to perform in-depth analyses of many subtle aspects related to Web interaction. Finally, the framework has been completely implemented in M...

• Type: Journal
• Year: 2009
• Where: FM
• Authors: María Alpuente, Demis Ballis, Daniel Romero
• Keywords: FM 2009, Formal Methods, Linear Temporal Logic, Scripting Languages, Web Scripting Languages