Summary
International Technical Conference on Circuits/Systems, Computers and Communications
2008
Session Number:H1
Session:
Number:H1-3
Formal Verification of Web Navigation by Symbolic Model Checking
Hisashi Miyazaki, Tomoyuki Yokogawa, Kouichi Seko, Yoichiro Sato, Michiyoshi Hayase,
pp.-
Publication Date:2008/7/7
Online ISSN:2188-5079
Summary:
Previously, it is general that users navigate from a web page to the other by clicking on a hyperlink. Recently web pages become dynamic with a variety of scripts and embedded client side programs. Such pages with dynamic navigation have a more complicated structure, so it is difficult to model and analyze. In this paper, we present a method to verify systems which have dynamic web navigation. For this purpose, we model the navigation using a UML statechart diagram and translate the model to a boolean expression. Thus it becomes possible to verify the systems formally using symbolic model checking. To demonstrate the proposed method, we apply the method to a system with dynamic web navigation and model-check the system using symbolic model checking tool called NuSMV. As a result, we verified reachability to all pages of the system.