Abstract
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.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-3-540-30232-2_24
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Online Dictionary and Search Engine for Computer and Internet Technology, http://www.pcwebopedia.com/
A glossary of World Wide Web Terminology, http://www-personal.umich.edu/~zoe/Glossary.html
W3C World Wide Web Consortium, http://www.w3.org
Graham, S.: HTML Sourcebook, A Complete Guide to HTML 3.0. John Wiley & Sons, Inc., Chichester (1996)
HTTP Proxy Server 1.0, http://www.reitshamer.com/source/httpproxy.html
HTTrack Website Copier, http://www.httrack.com/index.php
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)
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)
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)
Conallen, J.: Modeling Web Application Architectures, with UML. In: Proc. of Communications of the ACM, October 1999, vol. 2(10) (1999)
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)
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)
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)
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)
IEEE Computer Society, Software Reengineering Bibliography, October 28 (2002), http://www.informatik.uni-stuttgart.de/ifi/ps/reengineering
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)
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)
Ethereal, Network Protocol Analyzer, http://www.ethereal.com/
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Luotonen: Web Proxy Servers. Prentice Hall PTR, Englewood Cliffs (1998)
Krishnamurthy, Rexford, J.: Web Protocols and Practice: HTTP/1.1, Networking Protocols, Caching, and Traffic Measurement. Addison-Wesley, Reading (2001)
Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)
aSpin Model Checker, http://polaris.lcc.uma.es/gisum/fmse/tools/mainframe.html
Repository of Property Specification Patterns, http://patterns.projects.cis.ksu.edu/
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)
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)
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)
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)
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)
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)
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)
Wu, Y., Offutt, J.: Modeling and Testing Web-based Applications, GMU ISE Technical ISE-TR-02-08 (November 2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 IFIP International Federation for Information Processing
About this paper
Cite this paper
Haydar, M., Petrenko, A., Sahraoui, H. (2004). Formal Verification of Web Applications Modeled by Communicating Automata. In: de Frutos-Escrig, D., Núñez, M. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2004. FORTE 2004. Lecture Notes in Computer Science, vol 3235. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30232-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-30232-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23252-0
Online ISBN: 978-3-540-30232-2
eBook Packages: Springer Book Archive