Automated verification of pattern-based interaction invariants in Ajax applications

Yuta Maezawa, Hironori Washizaki, Yoshinori Tanabe, Shinichi Honiden

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

When developing asynchronous JavaScript and XML (Ajax) applications, developers implement Ajax design patterns for increasing the usability of the applications. However, unpredictable contexts of running applications might conceal faults that will break the design patterns, which decreases usability. We propose a support tool called JSVerifier that auto-matically verifies interaction invariants; the applications handle their interactions in invariant occurrence and order. We also present a selective set of interaction invariants derived from Ajax design patterns, as input. If the application behavior breaks the design patterns, JSVerifier automatically outputs faulty execution paths for debugging. The results of our case studies show that JSVerifier can verify the interaction invariants in a feasible amount of time, and we conclude that it can help developers increase the usability of Ajax applications.

Original languageEnglish
Title of host publication2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings
Pages158-168
Number of pages11
DOIs
Publication statusPublished - 2013 Dec 1
Event2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Palo Alto, CA, United States
Duration: 2013 Nov 112013 Nov 15

Publication series

Name2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings

Conference

Conference2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013
CountryUnited States
CityPalo Alto, CA
Period13/11/1113/11/15

    Fingerprint

Keywords

  • Ajax
  • Design Pattern
  • Model Checking
  • Reverse Engineering

ASJC Scopus subject areas

  • Software

Cite this

Maezawa, Y., Washizaki, H., Tanabe, Y., & Honiden, S. (2013). Automated verification of pattern-based interaction invariants in Ajax applications. In 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings (pp. 158-168). [6693076] (2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings). https://doi.org/10.1109/ASE.2013.6693076