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 forwa...

Full description

Saved in:
Bibliographic Details
Main Authors: Shengbo Chen, Huaikou Miao, Zhongsheng Qian
Format: Conference Proceeding
Language:English
Subjects:
Application software
Coverage criteria
History
Load modeling
Model checking
Navigation
Navigation models
Safety
Software design
Software engineering
Thyristors
Uniform resource locators
Web applications
Web browser interactions
Web pages
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1530-1362
2640-0715
DOI:10.1109/APSEC.2008.34