Modeling and Verifying Web Browser Interactions

Web applications can only be accessed through dedicated client systems called Web browsers. Most current Web browsers offer many tools or facilities for Web page revisiting, including the back and forward buttons, refresh, favorites, link menu and history lists etc. Users can press the back or forward buttons to negatively influence the behaviors of Web application navigation. Existing navigation models are static ones on the whole. Userspsila navigation paths are all determined on stage of model design. Web browser interactions have not been taken into account make them difference from practical navigation in Web applications. Accordingly, special care is taken on Web browser interactions during the userpsilas traversal within hypermedia space. We give out the concept of safety critical region (SCR) and propose an approach to modeling on-the-fly navigation models. The Kripke structure is employed to describe the on-the-fly navigation models. Coverage criteria of Web browser inter-actions, such as, node coverage, transition coverage triggered by actions, SCR coverage, are exploited to derive the properties of Web browser interactions in CTL. Ultimately, we use SMV, the model checking tool, to verify the on-the-fly navigation models.