TY - GEN
T1 - Automated verification of pattern-based interaction invariants in Ajax applications
AU - Maezawa, Yuta
AU - Washizaki, Hironori
AU - Tanabe, Yoshinori
AU - Honiden, Shinichi
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - Ajax
KW - Design Pattern
KW - Model Checking
KW - Reverse Engineering
UR - http://www.scopus.com/inward/record.url?scp=84893548562&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84893548562&partnerID=8YFLogxK
U2 - 10.1109/ASE.2013.6693076
DO - 10.1109/ASE.2013.6693076
M3 - Conference contribution
AN - SCOPUS:84893548562
SN - 9781479902156
T3 - 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings
SP - 158
EP - 168
BT - 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings
T2 - 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013
Y2 - 11 November 2013 through 15 November 2013
ER -