|
|
For Full-Text PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
|
Modeling, Verification and Testing of Web Applications Using Model Checker
Kei HOMMA Satoru IZUMI Kaoru TAKAHASHI Atsushi TOGASHI
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E94-D
No.5
pp.989-999
Publication Date: 2011/05/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E94.D.989
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Software Development Methodology
Keyword:
Web application, modeling, testing, automata, model checking, Spin,
Full Text: PDF>>
Summary:
The number of Web applications handling online transaction is increasing, but verification of the correctness of Web application development has been done manually. This paper proposes a method for modeling, verifying and testing Web applications. In our method, a Web application is modeled using two finite-state automata, i.e., a page automaton which specifies Web page transitions, and an internal state automaton which specifies internal state transitions of the Web application. General properties for checking the Web application design are presented in LTL formulae and they are verified using the model checker Spin. Test cases examining the behavior of the Web application are also generated by utilizing the counterexamples obtained as the result of model checking. We applied our method to an example Web application to confirm its effectiveness.
|
|
