Model Checking Web Applications Based On Web Navigation

With the development of web technologies and the increasing size of web sites, the structure of the web application becomes more complicated, and it becomes a difficult task to model and analyze it. Web navigation, which is useful for clarifying requirements and specifying implementation behavior, can be helpful in the analysis of web application. The structure of a web application can be checked based on the web navigation model. In this paper, we present a method to model and check a web application based on web navigation. We first model the web navigation by statechart, and then translate the statechart model to Promela description (the input language of SPIN), meanwhile, the properties to be checked are specified by LTL (Lineal Temporal Logic); finally the web navigation can be checked by SPIN. A case study demonstrates the advantages of our method.