Modeling and verification of Web applications using formal technique methods

Atsushi Togashi, Yuh Kitano, Satoru Izumi, Kaoru Takahashi, Kei Homma

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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. General assertions for checking Web application design are proposed, and a theoretical result for deadlock-freeness of Web application is also shown. An example Web application is modeled by the proposed method and checked using the model checker Spin.

Original languageEnglish
Title of host publicationProceedings - 2012 8th International Conference on Computing Technology and Information Management, ICCM 2012
Pages220-229
Number of pages10
Publication statusPublished - 2012
Event2012 8th International Conference on Computing Technology and Information Management, ICCM 2012 - Seoul, Korea, Republic of
Duration: 2012 Apr 242012 Apr 26

Publication series

NameProceedings - 2012 8th International Conference on Computing Technology and Information Management, ICCM 2012
Volume1

Conference

Conference2012 8th International Conference on Computing Technology and Information Management, ICCM 2012
Country/TerritoryKorea, Republic of
CitySeoul
Period12/4/2412/4/26

Keywords

  • Automata
  • Formal approach
  • Model Checking
  • Spin
  • Web application

Fingerprint

Dive into the research topics of 'Modeling and verification of Web applications using formal technique methods'. Together they form a unique fingerprint.

Cite this