An Approach for automated verification of web applications using model checking and replaying the scenarios of counterexamples

Thesis Type: Postgraduate

Institution Of The Thesis: Middle East Technical University, Turkey

Approval Date: 2015

Thesis Language: English

Student: Yudum Paçin

Consultant: AYSU BETİN CAN


The increase in the use of web applications in various domains, raised the importance of the methodologies for verification of web applications. We propose a framework for the verification of web applications with respect to access control, link consistency and reachability properties using model checking. In this approach, users define the properties by explanatory guidance of user interface. The execution traces that lead to a property violation is translated to a script that automates the replaying of the counterexample scenarios on a web browser. This facility enables the user to observe incorrect behaviors of the web application with respect to specified properties so that the user is released from the tedious task of understanding and interpreting the counterexamples generated by the model checker. In addition, to automate this verification process, we need to automate the model extraction of a web application to be given to the model checker as an input. To this purpose, we use two dynamic web application crawlers and automatically transform their models to an intermediate web model we have developed. This intermediate web model both enables model extraction tool independence and gives the user to edit the model manually to increase precision of verification process. In order to evaluate the tool we developed for this purpose, we conducted a user study and the participants reported our tool to be useful for detecting and visualizing errors. We also evaluated the effectiveness on real web applications and observed that the tool can reveal real faults.