Formal Verification of Web Applications Modeled by Communicating Automata

  • May Haydar
  • Alexandre Petrenko
  • Houari Sahraoui
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3235)


In this paper, we present an approach for modeling an existing web application using communicating finite automata model based on the user-defined properties to be validated. We elaborate a method for automatic generation of such a model from a recorded browsing session. The obtained model could then be used to verify properties with a model checker, as well as for regression testing and documentation. Unlike previous attempts, our approach is oriented towards complex multi-window/frame applications. We present an implementation of the approach that uses the model checker Spin and provide an example.


Model Checker Formal Verification Atomic Proposition Proxy Server Multiple Window 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Online Dictionary and Search Engine for Computer and Internet Technology,
  2. 2.
    A glossary of World Wide Web Terminology,
  3. 3.
    W3C World Wide Web Consortium,
  4. 4.
    Graham, S.: HTML Sourcebook, A Complete Guide to HTML 3.0. John Wiley & Sons, Inc., Chichester (1996)zbMATHGoogle Scholar
  5. 5.
  6. 6.
    HTTrack Website Copier,
  7. 7.
    Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proc. International Conference on Software Engineering (2000)Google Scholar
  8. 8.
    Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby: A, Language Framework For Expressing Checkable Properties of Dynamic Software. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Becker, S.A., Hevner, A.R.: A White Box Analysis of Concurrent System Designs. In: Proc. of the 10th Annual International Phoenix Conference on Computers and Communications, Scottsdale, AZ, USA, pp. 332–338 (1991)Google Scholar
  10. 10.
    Conallen, J.: Modeling Web Application Architectures, with UML. In: Proc. of Communications of the ACM, October 1999, vol. 2(10) (1999)Google Scholar
  11. 11.
    de Oliveira, M.C.F., Masiero, P.C.: A Statechart-Based Model for Hypermedia Applications. ACM Transactions on Information Systems 19(1), 28–52 (2001)CrossRefGoogle Scholar
  12. 12.
    Paulo, F.B., Masiero, P.C., de Olivieira, M.C.F.: Hypercharts: Extended Statecharts to Support Hypermedia Specification. IEEE Transactions on Software Engineering 25(1) (January 1999)Google Scholar
  13. 13.
    Paulo, F.B., Turine, M.A.S., de Olivieira, M.C.F.: XHMBS: a Formal Model to Support Hypermedia Specification. In: Proc. of the 9th ACM Conference on Hypertext, United Kingdom (June 1998)Google Scholar
  14. 14.
    Leung, K.R.P.H., Hui, L.C.K., Yui, S.M., Tang, R.W.M.: Modeling Web Navigation by Statechart. In: Proc. of the 24th IEEE Annual International Computer Software and Applications Conference, Taipei, Taiwan (October 2000)Google Scholar
  15. 15.
    IEEE Computer Society, Software Reengineering Bibliography, October 28 (2002),
  16. 16.
    Systä, T.: Static and Dynamic Reverse Engineering Techniques for Java Software Systems, Ph.D. dissertation, Dept. of Computer and Information Sciences, University of Tampere (2000)Google Scholar
  17. 17.
    Mansurov, N., Probert, R.: Dynamic Scenario-Based Approach to Re-Engineering of Legacy Telecommunication Systems. In: Proc. of the 9th SDL Forum (SDL 1999), Montreal, June 21–25, pp. 325–341 (1999)Google Scholar
  18. 18.
    Ethereal, Network Protocol Analyzer,
  19. 19.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  20. 20.
    Luotonen: Web Proxy Servers. Prentice Hall PTR, Englewood Cliffs (1998)Google Scholar
  21. 21.
    Krishnamurthy, Rexford, J.: Web Protocols and Practice: HTTP/1.1, Networking Protocols, Caching, and Traffic Measurement. Addison-Wesley, Reading (2001)Google Scholar
  22. 22.
    Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  23. 23.
  24. 24.
    Repository of Property Specification Patterns,
  25. 25.
    de Alfaro, L.: Model Checking the World Wide Web. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 337. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  26. 26.
    de Alfaro, L., Henziger, T.A., Mang, F.Y.C.: MCWEB: A Model-Checking Tool for Web Site Debugging. In: Poster, 10th WWW Conference, Hong Kong (2001)Google Scholar
  27. 27.
    Stotts, P.D., Cabarrus, C.R.: Hyperdocuments as Automata: Verification of Trace-Based Browsing Properties by Model Checking. ACM Transactions on Information Systems 16(1), 1–30 (1998)CrossRefGoogle Scholar
  28. 28.
    Stotts, P.D., Navon, J.: Model Checking CobWeb Protocols for Verification of HTML Frames Behavior. In: Proc. of the 11th WWW Conference, Hawai, U.S.A. (May 2002)Google Scholar
  29. 29.
    Ricca, F., Tonella, P.: Web Site Analysis: Structure and Evolution. In: Proc. of International Conference on Software Maintenance (ICSM 2000), San Jose, California, USA, October 11-14, pp. 76–86 (2000)Google Scholar
  30. 30.
    Ricca, F., Tonella, P.: Analysis and Testing of Web Applications. In: Proc. of the International Conference on Software Engineering (ICSE 2001), Toronto, Ontario, Canada, May 12-19, pp. 25–34 (2001)Google Scholar
  31. 31.
    Tonella, P., Ricca, F.: Dynamic Model Extraction and Statistical Analysis of Web Applications. In: Proc. of International Workshop on Web Site Evolution (WSE 2002), Montreal, Canada, October 2, pp. 43–52 (2002)Google Scholar
  32. 32.
    Wu, Y., Offutt, J.: Modeling and Testing Web-based Applications, GMU ISE Technical ISE-TR-02-08 (November 2002)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2004

Authors and Affiliations

  • May Haydar
    • 1
    • 2
  • Alexandre Petrenko
    • 1
  • Houari Sahraoui
    • 2
  1. 1.CRIM, Centre de recherche informatique de MontréalMontrealCanada
  2. 2.Département d’informatique et de recherche opérationnelleUniversité de MontréalMontrealCanada

Personalised recommendations