• DocumentCode
    2519972
  • Title

    Using the Model Checker Spin for Web Application Design

  • Author

    Homma, Kei ; Izumi, Satom ; Abe, Yuki ; Takahashi, Kaom ; Togashi, Atsushi

  • Author_Institution
    Grad. Sch. of Project Design, Miyagi Univ., Sendai, Japan
  • fYear
    2010
  • fDate
    19-23 July 2010
  • Firstpage
    137
  • Lastpage
    140
  • 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.
  • Keywords
    Internet; Web design; formal verification; transaction processing; Web application design; finite state automata; model checker spin; online transaction; verification; Automata; Business; Computational modeling; Educational institutions; System recovery; Unified modeling language; Web pages; Model Checking; Spin; Web Application;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Applications and the Internet (SAINT), 2010 10th IEEE/IPSJ International Symposium on
  • Conference_Location
    Seoul
  • Print_ISBN
    978-1-4244-7526-1
  • Electronic_ISBN
    978-0-7695-4107-5
  • Type

    conf

  • DOI
    10.1109/SAINT.2010.73
  • Filename
    5598158
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2519972