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
    Event2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Palo Alto, CA
    Duration: 2013 Nov 112013 Nov 15

    Other

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

    Fingerprint

    XML

    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] https://doi.org/10.1109/ASE.2013.6693076

    Automated verification of pattern-based interaction invariants in Ajax applications. / Maezawa, Yuta; Washizaki, Hironori; Tanabe, Yoshinori; Honiden, Shinichi.

    2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings. 2013. p. 158-168 6693076.

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

    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., 6693076, pp. 158-168, 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013, Palo Alto, CA, 13/11/11. https://doi.org/10.1109/ASE.2013.6693076
    Maezawa Y, Washizaki H, Tanabe Y, Honiden S. Automated verification of pattern-based interaction invariants in Ajax applications. In 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings. 2013. p. 158-168. 6693076 https://doi.org/10.1109/ASE.2013.6693076
    Maezawa, Yuta ; Washizaki, Hironori ; Tanabe, Yoshinori ; Honiden, Shinichi. / Automated verification of pattern-based interaction invariants in Ajax applications. 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings. 2013. pp. 158-168
    @inproceedings{f8ffb309ec01459da748de5ef08b136a,
    title = "Automated verification of pattern-based interaction invariants in Ajax applications",
    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.",
    keywords = "Ajax, Design Pattern, Model Checking, Reverse Engineering",
    author = "Yuta Maezawa and Hironori Washizaki and Yoshinori Tanabe and Shinichi Honiden",
    year = "2013",
    doi = "10.1109/ASE.2013.6693076",
    language = "English",
    isbn = "9781479902156",
    pages = "158--168",
    booktitle = "2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings",

    }

    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

    SP - 158

    EP - 168

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

    ER -