This paper presents a Rewriting Logic framework that formalizes the interactions between Web servers and Web browsers through a communicating
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 win- dow/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 suit- able 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 Maude,
and we report on some successful experiments that we conducted by using the Maude LTLR model-checker.
