User Tools

Site Tools


This is an old revision of the document!


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 automatically 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.


Yann-Gaël Guéhéneuc, 2013/01/08

Following their previous work on extracting state-machines from AJAX applications, the authors proposed a Spin-based tool to verify invariants in AJAX state machines. The paper is very interesting and its treatment thorough. The paper starts by saying that AJAX is “credited with the 500% increase in Web users compared to a decade ago.”, the main factor being the improved user experience with rich Web application, i.e., their usability. However, “unpredictable contexts while running application might conceal faults that will break the design patterns” used by developers to ensure usability.

automated_verification_of_pattern-based_interaction_invariants_in_ajax_applications.1389189656.txt.gz · Last modified: 2018/03/04 02:53 (external edit)