Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - 2010 10th Annual International Symposium on Applications and the Internet, SAINT 2010 |
| Pages | 137-140 |
| Number of pages | 4 |
| DOIs | |
| Publication status | Published - 2010 Nov 29 |
| Event | 2010 10th Annual International Symposium on Applications and the Internet, SAINT 2010 - Seoul, Korea, Republic of Duration: 2010 Jul 19 → 2010 Jul 23 |
Publication series
| Name | Proceedings - 2010 10th Annual International Symposium on Applications and the Internet, SAINT 2010 |
|---|
Other
| Other | 2010 10th Annual International Symposium on Applications and the Internet, SAINT 2010 |
|---|---|
| Country | Korea, Republic of |
| City | Seoul |
| Period | 10/7/19 → 10/7/23 |
Keywords
- Model checking
- Spin
- Web application
ASJC Scopus subject areas
- Computer Networks and Communications
- Computer Science Applications
Fingerprint Dive into the research topics of 'Using the model checker spin for web application design'. Together they form a unique fingerprint.
Cite this
Homma, K., Izumi, S., Abe, Y., Takahashi, K., & Togashi, A. (2010). Using the model checker spin for web application design. In Proceedings - 2010 10th Annual International Symposium on Applications and the Internet, SAINT 2010 (pp. 137-140). [5598158] (Proceedings - 2010 10th Annual International Symposium on Applications and the Internet, SAINT 2010). https://doi.org/10.1109/SAINT2010.73