http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
Formal Verification of Web Navigation by Symbolic Model Checking
Hisashi MIYAZAKI,Tomoyuki YOKOGAWA,Kouichi SEKO,Yoichiro SATO,Michiyoshi HAYASE 대한전자공학회 2008 ITC-CSCC :International Technical Conference on Ci Vol.2008 No.7
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.