Using the Model Checker Spin for Web Application Design
説明
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.
収録刊行物
-
- 2010 10th IEEE/IPSJ International Symposium on Applications and the Internet
-
2010 10th IEEE/IPSJ International Symposium on Applications and the Internet 137-140, 2010-07-01
IEEE