More Web Proxy on the site http://driver.im/

Article

Runtime verification for the web: a tutorial introduction to interface contracts in web applications

Authors:

Sylvain Hallé,

Roger VillemaireAuthors Info & Claims

RV'10: Proceedings of the First international conference on Runtime verification

Pages 106 - 121

Published: 01 November 2010 Publication History

Abstract

This tutorial presents an introduction to the monitoring of web applications. These applications run in a user's web browser and exchange requests and responses with a server in the background to update their display. A demo application, called the Beep Store, illustrates why complex properties on this exchange must be verified at runtime. These properties can be formalized using an extension of Linear Temporal Logic called LTL-FO+. The tutorial concludes with the presentation of BeepBeep, a lightweight runtime monitor for web applications.

References

[1]

Amazon e-commerce service, http://solutions.amazonwebservices.com

[2]

Paypal web service API documentation, http://www.paypal.com

[3]

Apache Axis (2010), http://ws.apache.org/axis2

[4]

ASE 2010, 25th IEEE/ACM International Conference on Automated Software Engineering, Antwerp, Belgium, September 20-24. IEEE Computer Society, Los Alamitos (2010).

[5]

Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services, Concepts, Architectures and Applications, p. 354. Springer, Heidelberg (2004).

[6]

Barringer, H., Havelund, K., Rydeheard, D.E., Groce, A.: Rule systems for runtime verification: A short tutorial. In: Bensalem, S., Peled, D. (eds.) RV 2009. LNCS, vol. 5779, pp. 1-24. Springer, Heidelberg (2009).

Digital Library

[7]

Boutaba, R., Golab, W., Iraqi, Y., Arnaud, B.S.: Lightpaths on demand: A web-services-based management system. IEEE Communications Magazine, 2-9 (July 2004).

Digital Library

[8]

Chen, F., d'Amorim, M., Rosu, G.: Checking and correcting behaviors of java programs at runtime with Java-MOP. Electr. Notes Theor. Comput. Sci. 144(4), 3-20 (2006).

Digital Library

[9]

Christensen, E., Curbera, F., Meredith, G., Weerawarana, S.: Web services description language (WSDL) 1.1, W3C note (2001).

[10]

Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) PSTV. IFIP Conference Proceedings, vol. 38, pp. 3-18. Chapman & Hall, Boca Raton (1995).

Digital Library

[11]

Hallé, S.: Cooperative runtime monitoring of LTL interface contracts. In: EDOC. IEEE Computer Society, Los Alamitos (to appear, October 2010).

Digital Library

[12]

Hallé, S., Bultan, T., Hughes, G., Alkhalaf, M., Villemaire, R.: Runtime verification of web service interface contracts. IEEE Computer 43(3), 59-66 (2010).

Digital Library

[13]

Hallé, S., Ettema, T., Bunch, C., Bultan, T.: Eliminating navigation errors in web applications via model checking and runtime enforcement of navigation state machines. In: ASE {4} (2010).

Digital Library

[14]

Hallé, S., Hughes, G., Bultan, T., Alkhalaf, M.: Generating interface grammars from WSDL for automated verification of web services. In: Baresi, L., Chi, C.-H., Suzuki, J. (eds.) ICSOC-Service Wave 2009. LNCS, vol. 5900, pp. 516-530. Springer, Heidelberg (2009).

Digital Library

[15]

Hallé, S., Villemaire, R.: Runtime monitoring of message-based workflows with data. In: EDOC, pp. 63-72. IEEE Computer Society, Los Alamitos (2008).

Digital Library

[16]

Hallé, S., Villemaire, R.: Browser-based enforcement of interface contracts in web applications with BeepBeep. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol. 5643, pp. 648-653. Springer, Heidelberg (2009).

Digital Library

[17]

Hallé, S., Villemaire, R.: Runtime monitoring of web service choreographies using streaming XML. In: Shin, S.Y., Ossowski, S. (eds.) SAC, pp. 2118-2125. ACM, New York (2009).

Digital Library

[18]

Hallé, S., Villemaire, R.: XML query evaluation in validation and monitoring of web service interface contracts. In: advanced Applications and Structures in XML Processing: Label Streams, Semantics Utilization and Data Query Technologies, pp. 406-424. IGI Global (2010).

[19]

Hallé, S., Villemaire, R., Cherkaoui, O.: Specifying and validating data-aware temporal web service properties. IEEE Trans. Software Eng. 35(5), 669-683 (2009).

Digital Library

[20]

Mitra, N., Lafon, Y.: SOAP version 1.2 part 0: Primer, 2nd edn. (2007), http://www.w3.org/TR/2007/REC-soap12-part0-20070427

Cited By

Schiavio FSun HBonetta DRosà ABinder WHung CPapadopoulos G(2019)NodeMOPProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297456(1794-1801)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297456
Bauer AFalcone Y(2016)Decentralised LTL monitoringFormal Methods in System Design10.1007/s10703-016-0253-848:1-2(46-93)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1007/s10703-016-0253-8
Hallé SVillemaire RLago PLewis GMetzger ATosic V(2012)Constraint-based invocation of stateful web servicesProceedings of the 4th International Workshop on Principles of Engineering Service-Oriented Systems10.5555/2666048.2666059(61-62)Online publication date: 4-Jun-2012
https://dl.acm.org/doi/10.5555/2666048.2666059

Recommendations

Intelligent crawling of web applications for web archiving
WWW '12 Companion: Proceedings of the 21st International Conference on World Wide Web

The steady growth of the World Wide Web raises challenges regarding the preservation of meaningful Web data. Tools used currently by Web archivists blindly crawl and store Web pages found while crawling, disregarding the kind of Web site currently ...
Collaborative runtime verification with tracematches
RV'07: Proceedings of the 7th international conference on Runtime verification

Perfect pre-deployment test coverage is notoriously difficult to achieve for large applications. With enough end users, many more test cases will be encountered during an application's deployment than during testing. The use of runtime verification ...
Modeling Web Applications Design with Automata and Its Verification
ISADS '11: Proceedings of the 2011 Tenth International Symposium on Autonomous Decentralized Systems

The number of Web applications handling online transaction is increasing, but verication of the correctness of the Web application design has been done manually. This paper proposes a method for modeling Web applications using two nite-state automata, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

RV'10: Proceedings of the First international conference on Runtime verification

November 2010

491 pages

ISBN:3642166113

Editors:
Howard Barringer
University of Manchester, UK
,
Ylies Falcone
IRISA, INRIA, Rennes, France
,
Bernd Finkbeiner
Saarland University, Saarücken, Germany
,
Klaus Havelund
Jet Propulsion Laboratory, Pasadena, CA
,
Insup Lee
University of Pennsylvania, Philadelphia, PA

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 November 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Schiavio FSun HBonetta DRosà ABinder WHung CPapadopoulos G(2019)NodeMOPProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297456(1794-1801)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297456
Bauer AFalcone Y(2016)Decentralised LTL monitoringFormal Methods in System Design10.1007/s10703-016-0253-848:1-2(46-93)Online publication date: 1-Apr-2016
https://dl.acm.org/doi/10.1007/s10703-016-0253-8
Hallé SVillemaire RLago PLewis GMetzger ATosic V(2012)Constraint-based invocation of stateful web servicesProceedings of the 4th International Workshop on Principles of Engineering Service-Oriented Systems10.5555/2666048.2666059(61-62)Online publication date: 4-Jun-2012
https://dl.acm.org/doi/10.5555/2666048.2666059

View Options

View options

Media

Figures

Other

Tables

View Table of Contents