automated_verification_of_pattern-based_interaction_invariants_in_ajax_applications
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
automated_verification_of_pattern-based_interaction_invariants_in_ajax_applications [2014/01/08 14:24] yann |
automated_verification_of_pattern-based_interaction_invariants_in_ajax_applications [2014/01/08 14:26] yann |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| 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. | 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? | ||
automated_verification_of_pattern-based_interaction_invariants_in_ajax_applications.txt ยท Last modified: 2019/10/06 20:37 (external edit)
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Share Alike 4.0 International
