Abstract
Web-TLR is a software tool designed for model-checking Web applications which is based on rewriting logic. Web applications are expressed as rewrite theories which can be formally verified by using the Maude built-in LTLR model-checker. Web-TLR is equipped with a user-friendly, graphical Web interface that shields the user from unnecessary information. Whenever a property is refuted, an interactive slideshow is generated that allows the user to visually reproduce, step by step, the erroneous navigation trace that underlies the failing model checking computation. This provides deep insight into the system behavior, which helps to debug Web applications.
This work has been partially supported by the EU (FEDER) and the Spanish MEC TIN2007-68093-C02-02 project, by Generalitat Valenciana, under grant Emergentes GV/2009/024, and by the Italian MUR under grant RBIN04M8S8, FIRB project, Internationalization 2004. Daniel Romero is also supported by FPI–MEC grant BES–2008–004860.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alalfi, M.H., Cordy, J.R., Dean, T.R.: Modelling Methods for Web Application Verification and Testing: State of the Art. Software Testing, Verification and Reliability 19, 265–296 (2009)
Alpuente, M., Ballis, D., Romero, D.: Specification and Verification of Web Applications in Rewriting Logic. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 790–805. Springer, Heidelberg (2009)
Bae, K., Meseguer, J.: A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting. In: Proc. of the 9th International Workshop on Rule-Based Programming (RULE 2008). ENTCS. Elsevier, Amsterdam (2008)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Flores, S., Lucas, S., Villanueva, A.: Formal verification of websites. In: Proc. 4th Int’l Workshop on Automated Specification and Verification of Web Sites (WWV 2008). ENTCS, vol. 200(3), pp. 103–118 (2008)
Graunke, P., Findler, R., Krishnamurthi, S., Felleisen, M.: Modeling web interactions. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 238–252. Springer, Heidelberg (2003)
Haydar, M., Sahraoui, H., Petrenko, A.: Specification patterns for formal web verification. In: ICWE 2008: Proc. of the 2008 Eighth International Conference on Web Engineering, pp. 240–246. IEEE CS, Los Alamitos (2008)
Meseguer, J.: The Temporal Logic of Rewriting: A Gentle Introduction. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 354–382. Springer, Heidelberg (2008)
Message, R., Mycroft, A.: Controlling control flow in web applications. In: Proc. 4th Int’l Workshop on Automated Specification and Verification of Web Sites (WWV 2008). ENTCS, vol. 200(3), pp. 119–131 (2008)
Miao, H., Zeng, H.: Model checking-based verification of web application. In: ICECCS 2007: Proc. of the 12th IEEE Int’l Conf. on Engineering Complex Computer Systems (ICECCS 2007), Washington, DC, USA, pp. 47–55. IEEE CS, Los Alamitos (2007)
Queinnec, C.: Continuations and web servers. Higher-Order and Symbolic Computation 17(4), 277–295 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alpuente, M., Ballis, D., Espert, J., Romero, D. (2010). Model-Checking Web Applications with Web-TLR . In: Bouajjani, A., Chin, WN. (eds) Automated Technology for Verification and Analysis. ATVA 2010. Lecture Notes in Computer Science, vol 6252. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15643-4_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-15643-4_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15642-7
Online ISBN: 978-3-642-15643-4
eBook Packages: Computer ScienceComputer Science (R0)