Slicing-based debugging of web applications in rewriting logic

Abstract

The pervasiveness of computing on the Internet has led to an explosive growth of Web applications that, together with their ever-increasing complexity, have turned their design and development in a major challenge. Unfortunately, the huge expansion of development and utilization of Web computation has not been paired by the development of methods, models and debugging tools to help the developer diagnose, quickly and easily, potential problems in a Web application. There is an urgent demand of analysis and verification facilities capable to prevent insecure software that could cause unavailability of systems or services, or provide access to private data or internal resources of a given organization. The main goal of this MSc thesis is to improve the debugging of Web applications by embedding novel analysis and verification techniques that rely on the program semantics. As a practical realization of the ideas, we use Web-TLR that is a verification engine for dynamic Web applications based on Rewrite Logic. We extend Web-TLR with a novel functionality that supports effective Web debugging for realistic Web applications involving complex execution traces. This functionality is based on a backward trace slicing technique that is based on dynamic labeling. In order to extend the class of programs covered by the debugging methodology we formalize a generalization of the slicer to Conditional Rewriting Logic theories, greatly simplifying the debugging task by providing a novel and sophisticated form of pattern matching.