@proceedings {ABR09,
	title = {Specification and Verification of Web Applications in Rewriting Logic},
	journal = {16th International Symposium on Formal Methods, FM 2009},
	year = {2009},
	pages = {790{\textendash}805},
	publisher = {Springer},
	abstract = {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 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 Maude, and we report on some successful experiments  that we  conducted by using the Maude LTLR model-checker.},
	keywords = {Model-checking, Rewriting Logic, Specification of Web Applications, Verification of Web Applications},
	author = {Maria Alpuente and Demis Ballis and Daniel Omar Romero}
}
