A model checking approach to Web application navigation model with session mechanism

It is important to ensure the reliability of Web applications at early design phase. Model checking is a viable method to achieve this goal. In this paper, we analyze the interaction between the Web application and browser and propose a method to formal modeling and verify Web application navigation model with session mechanism. We use UML sequence diagram to express the interaction between user and browser. Then properties of the Web application navigation model are specified in CTL formulas and an automated model checking tool, NuSMV is employed to perform automated verification. An example is given to demonstrate how our approach can uncover navigations problems with session mechanism.