http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
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.
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.