A verification method for some GUI dialogue properties
Yoshihiro Tsujino · Systems and Computers in Japan · 2000
I propose a GUI dialogue model and an automatic verification method in order to verify properties of reachability and unreachability. Conventional GUI models such as finite state machines, used for GUI verification, have problems of insufficient descriptive power, computational and/or descriptive state explosions, and difficulty in solving the unreachability problems. The proposed model and method are more powerful in practice, easy to use, and based on the concept of the weakest precondition which is used in the area of program verification. I also implemented a prototype of the GUI verifier with the proposed method. © 2000 Scripta Technica, Syst Comp Jpn 31(14): 38–46, 2000