Modeling and verification of adaptive navigation in web applications

ABSTRACT

The navigation of a web application is the possible sequences of web pages a user can visit. In the simplest case the next page is determined by the current page and the action (e.g. link, button) selected by the user. However, many web applications now incorporate adaptive navigation, where the next page also depends on the user's mode, for example whether they are a customer or an administrator, or depends on what pages the user has visited previously.Navigation models are useful for clarifying requirements and specifying implementation behavior. When a model is formal, it can also be used to generate design or implementation artifacts, and can be verified for properties such as broken links or length of navigation path. These uses are all important for the case of simple navigation, but even more important for adaptive navigation because of the added complexity. However, none of the current formal approaches can support adaptive navigation.In this paper we present an approach that uses Statecharts to formally model adaptive navigation, and show how important properties of a navigation model are verified using existing model-checking tools. We summarize the kinds of properties that can be checked with such a model, and describe how to use the Symbolic Model Verifier (SMV) tool to perform the verification. Finally, we use the Blockbuster® web site as a case study to demonstrate how our approach can uncover navigation problems that arise when new requirements are imposed.

REFERENCES

• 1: William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998 [doi>10.1109/32.708566 ]
• 2: Luca de Alfaro, Model Checking the World Wide Web, Proceedings of the 13th International Conference on Computer Aided Verification, p.337-349, July 18-22, 2001
• 3: Baumeister, H., Knapp, A., Koch, Nora, and Zhang, G. Modelling Adaptivity with Aspects. Proceedings of ICWE, Springer-Verlag, 2005, 406--416.
• 4: Matthias Book , Volker Gruhn, Modeling Web-Based Dialog Flows for Automatic Dialog Control, Proceedings of the 19th IEEE international conference on Automated software engineering, p.100-109, September 20-24, 2004 [doi>10.1109/ASE.2004.51]
• 5: Sven Casteleyn , Olga De Troyer , Saar Brockmans, Design time support for adaptive behavior in Web sites, Proceedings of the 2003 ACM symposium on Applied computing, March 09-12, 2003, Melbourne, Florida [doi>10.1145/952532.952769]
• 6: Ceri, S., Daniel, F., Demaldé, V., and Facca, F. M. An Approach to User-Behavior-Aware Web Applications. Proceedings of ICWE, Springer-Verlag, 2005, 417--428.
• 7: Stefano Ceri , Piero Fraternali , Aldo Bongio, Web Modeling Language (WebML): a modeling language for designing Web sites, Proceedings of the 9th international World Wide Web conference on Computer networks : the international journal of computer and telecommunications netowrking, p.137-157, June 2000, Amsterdam, The Netherlands
• 8: Jim Conallen, Building Web Applications with Uml, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 9: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 10: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 11: Han, M., and Hofmeister, C. Modeling Navigation Routing in J2EE Web Applications. Lehigh Univ. Tech. Report,2004.
• 12: Han, M., and Hofmeister, C. Separation of Navigation Routing Code in J2EE Web Applications. Proceedings of ICWE, 2005. pp 221--231.
• 13: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9 ]
• 14: David Harel , Amnon Naamad, The STATEMATE semantics of statecharts, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.293-333, Oct. 1996 [doi>10.1145/235321.235322]
• 15: Koch, N., Baumeister, H., Hennicker, R. and Mandel, L. Extending UML to Model Navigation and Presentation in Web Applications. Workshop on Modelling Web Applications in UML, UML 2000, York, UK, (Oct 2000).
• 16: Karl R. P. H. Leung , Lucas Chi Kwong Hui , S. M. Yiu , Ricky W. M. Tang, Modeling Web Navigation by Statechart, 24th International Computer Software and Applications Conference, p.41-47, October 25-28, 2000
• 17: Daniel R. Licata , Shriram Krishnamurthi, Verifying Interactive Web Programs, Proceedings of the 19th IEEE international conference on Automated software engineering, p.164-173, September 20-24, 2004 [doi>10.1109/ASE.2004.76]
• 18: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 19: Paolo Merialdo , Paolo Atzeni , Giansalvatore Mecca, Design and development of data-intensive web sites: The Araneus approach, ACM Transactions on Internet Technology (TOIT), v.3 n.1, p.49-92, February 2003 [doi>10.1145/643477.643480]
• 20: Maria Cristina Ferreira de Oliveira , Marcelo Augusto Santos Turine , Paulo Cesar Masiero, A statechart-based model for hypermedia applications, ACM Transactions on Information Systems (TOIS), v.19 n.1, p.28-52, Jan. 2001 [doi>10.1145/366836.366869]
• 21: Mike Perkowitz , Oren Etzioni, Towards adaptive Web sites: conceptual framework and case study, Artificial Intelligence, v.118 n.1-2, p.245-275, April 2000 [doi>10.1016/S0004-3702(99)00098-3 ]
• 22: Rational Software. Pearl Circle Online Auction Reference Application Software Architecture Document, Issue 0.2. Rational Software 2001.
• 23: Filippo Ricca , Paolo Tonella, Analysis and testing of Web applications, Proceedings of the 23rd International Conference on Software Engineering, p.25-34, May 12-19, 2001, Toronto, Ontario, Canada
• 24: Daniel Schwabe , Gustavo Rossi, An object oriented approach to Web-based applications design, Theory and Practice of Object Systems, v.4 n.4, p.207-225, Oct. 12, 1998 [doi>10.1002/(SICI)1096-9942(1998)4:4<207::AID-TAPO2>3.0.CO;2-2 ]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: State diagrams

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Design, Documentation, Verification

Keywords:
adaptive navigation, navigation model, web application