Formal Verification of Web Navigation by Symbolic Model Checking
Hisashi Miyazaki, Tomoyuki Yokogawa, Kouichi Seko, Yoichiro Sato, Michiyoshi Hayase · ITC-CSCC :International Technical Conference on Circuits Systems, Computers and Communications · 2008
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 [9]. As a result, we verified reachability to all pages of the system.