TY - GEN
T1 - Using the model checker spin for web application design
AU - Homma, Kei
AU - Izumi, Satom
AU - Abe, Yuki
AU - Takahashi, Kaom
AU - Togashi, Atsushi
N1 - Copyright:
Copyright 2010 Elsevier B.V., All rights reserved.
PY - 2010
Y1 - 2010
N2 - The number of Web applications handling online transaction is increasing, but verification of the correctness of the Web application design has been done manually. This paper proposes a method for modeling Web applications 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. An example Web application is modeled by the proposed method and checked using the model checker Spin.
AB - The number of Web applications handling online transaction is increasing, but verification of the correctness of the Web application design has been done manually. This paper proposes a method for modeling Web applications 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. An example Web application is modeled by the proposed method and checked using the model checker Spin.
KW - Model checking
KW - Spin
KW - Web application
UR - http://www.scopus.com/inward/record.url?scp=78649291889&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78649291889&partnerID=8YFLogxK
U2 - 10.1109/SAINT2010.73
DO - 10.1109/SAINT2010.73
M3 - Conference contribution
AN - SCOPUS:78649291889
SN - 9780769541075
T3 - Proceedings - 2010 10th Annual International Symposium on Applications and the Internet, SAINT 2010
SP - 137
EP - 140
BT - Proceedings - 2010 10th Annual International Symposium on Applications and the Internet, SAINT 2010
T2 - 2010 10th Annual International Symposium on Applications and the Internet, SAINT 2010
Y2 - 19 July 2010 through 23 July 2010
ER -