Rewriting-based Verification and Debugging of Web Systems

• Autores: Daniel Omar Romero
• Directores de la Tesis: María Alpuente Frasnedo (dir. tes.) , Demis Ballis (dir. tes.)
• Lectura: En la Universitat Politècnica de València ( España ) en 2011
• Idioma: inglés
• Tribunal Calificador de la Tesis: Salvador Lucas Alba (presid.) , Francisco Javier Oliver Villarroya (secret.) , Massimo Marchiori (voc.) , Moreno Falaschi (voc.) , María del Mar Gallardo Melgarejo (voc.)
• Enlaces
  • Tesis en acceso abierto en: RiuNet
• Resumen

  • The increasing complexity of Web system has led to the development of sophisticated formal methodologies for verifying and correcting Web data and Web programs. In general, establishing whether a Web system behaves correctly with respect to the original intention of the programmer or checking its internal consistency are non-trivial tasks as witnessed by many studies in the literature. In this dissertation, we face two challenging problems related to the verification of Web systems. Firstly, we extend a previous Web verification framework based on partial rewriting by providing a semi-automatic technique for repairing Web systems. We propose a basic repairing methodology that is endowed with several strategies for optimizing the number of repair actions that must be executed in order to fix a given Web site. Also, we develop an improvement of the Web verification framework that is based on abstract interpretation and greatly enhances both efficiency and scalability of the original technique. Secondly, we formalize a framework for the specification and model-checking of dynamic Web applications that is based on Rewriting Logic. Our framework allows one to simulate the user navigation and the evaluation of Web scripts within a Web application, and also check important related properties such us reachability and consistency. When a property is refuted, a counter-example with the erroneous trace is delivered. Such information can be analyzed in order to debug the Web application under examination by means of a novel backward trace slicing technique that we formulated for this purpose. This technique consists in tracing back, along an execution trace, all the relevant symbols of the term (or state) that we are interested to observe.