Ptidej Team WIki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Maezawa, Y.; Washizaki, H.; Tanabe, Y. & Honiden, S. Automated Verification of Pattern-based Interaction Invariants in Ajax Applications. Proceedings of the 28th International Conference on Automated Software Engineering, IEEE CS Press, 2013 ======

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

===== Comments =====

//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. "By leveraging an AJAX engine on the client side, the applications can asynchronously receive necessary data from servers and partially update a Web page without page transitions", thus improving user experience. To improve user experience, developers are concerned with the interactions that the applications can handle (from users, servers, and themselves) and the behaviour of the applications when handling these interactions but also the behaviour when enabling and disabling interactions. However, due to unpredictable contexts (such as network speed or other AJAX scripts), "developers may miss certain paths to be executed, which can result in unexpected behaviour".

Consequently, the paper presents JSVerifier and the steps used (1) to extract a state machine from a set of JavaScript, CSS, and HTML files and (2) to analyse this state machine to verify invariants. The steps require also some manual inputs because parsers cannot distinguish event attributes, callback objects, event handling functions, and control attributes, "developers [must] define these elements relevant to [the] interactions [...] in distinguishing rules". Then, JSVerifier can "[create] relationship between invoked functions and callback functions". It can also abstract the call graph, also this part is rather obscure, and finally refine the relationships among interactions. Then, JSVerifier translate the refined, abstract call graphs into Promela model for SPIN. It requires interaction invariants hand-written to act as verification formulas. These interaction invariants are extracted from AJAX usability design patterns, for example "user event registration". Finally, JSVerifier can output the result of the verification and a counter-example if appropriate. The paper shows that, on three examples, JSVerifier runs with acceptable time although the examples were such that no (real) counter-examples were found.

The paper raises interesting questions, in particular with respect to the manual tagging of the call graph and the translation of the usability design patterns into interactions invariants: could the manual tagging be made automatic and can any design pattern be translated into an interaction invariant?