Structural modeling and verification of web applications

The complex structure and rapid development of web applications can lead to vulnerabilities and flaws that can compromise sensitive data. Detecting these vulnerabilities at the early stages of development cycle ensures that they are easier and cheaper to fix. Structural modeling of web applications is becoming increasingly important for detection, and subsequent elimination of such flaws. In this paper we analyze structural models of web applications. We use the model checking tools Spin and Uppaal to model dynamic navigation flow. We simulate and verify time-bound navigation properties by examining the sequence of actions that a user would make when interacting with the application. We compare the usefulness of the modeling tools for analysis of users’ behavior.