Title
Using the Model Checker Spin for Web Application Design
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.
Year
DOI
Venue
2010
10.1109/SAINT.2010.73
SAINT
Keywords
Field
DocType
internal state automaton,finite-state automaton,model checker spin,page automaton,web application design,internal state transition,web page transition,web application,example web application,computational modeling,web pages,formal verification,verification,finite state automata,transaction processing,automata,unified modeling language,model checking,internet,spin,state transition,business,web design
Web design,Programming language,Model checking,Web page,Computer science,Correctness,Theoretical computer science,Finite-state machine,Rewrite engine,Web application,Formal verification
Conference
Citations 
PageRank 
References 
4
0.43
4
Authors
5
Name
Order
Citations
PageRank
Kei Homma181.17
Satoru Izumi2366.80
Yuki Abe340.43
Kaoru Takahashi4305.27
Atsushi Togashi57113.34