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.
A tool support for verifying consistency between UML diagrams by SMV
Shinji HARADA,Tomoyuki YOKOGAWA,Hisashi MIYAZAKI,Yoichiro SATO,Michiyoshi HAYASE 대한전자공학회 2009 ITC-CSCC :International Technical Conference on Ci Vol.2009 No.7
We develop a tool to support verification of consistency between designs described by UML diagrams. This tool translates an XML data exported from a UML drawer into an input of SMV (called SMV program). This tool provides afront-end which parses an XML data and generates an intermediate data. This tool also provides a back-end which generates an SMV programfrom the intermediate data. We show the availability of our tool by applying it to an example.