自动验证GUI对话框属性的方法

需积分: 5 131 浏览量更新于2024-08-07 收藏 165KB PDF 举报

"A verification method for some GUI dialogue properties - Yoshihiro Tsujino - Kyoto Institute of Technology - GUI dialogue model - Automatic verification - Reachability and unreachability properties - Finite state machines - Unreachability problems - Weakest precondition concept - Program verification - Prototype implementation" 这篇论文提出了一种图形用户界面（GUI）对话框的验证方法，旨在验证可达性和不可达性的属性。作者Yoshihiro Tsujino来自京都工艺工业大学的信息与生产科学研究生院，该研究解决了在GUI设计中的一些关键问题。传统的GUI模型，如有限状态机，常用于GUI的验证，但存在描述能力不足、计算复杂性爆炸以及解决不可达性问题的困难。论文中提出的新型GUI对话框模型和自动验证方法在实践中更强大，使用更为简便，并且基于程序验证领域中的最弱前条件概念。最弱前条件在程序验证中被广泛使用，可以帮助确定程序执行前必须满足的条件。此外，作者还实现了一个基于该提议方法的GUI验证器原型。这表明该方法不仅停留在理论层面，而且可以实际应用于软件开发过程中，提高GUI软件的质量和效率。关键词包括：GUI设计、对话框模型、形式化规范、自动验证、可达性问题。这些关键词强调了研究的核心内容，即通过形式化的方法改进GUI的验证过程，以确保其功能的正确性和用户的可访问性。在介绍部分，论文指出创建高质量的GUI软件是一项既困难又昂贵的任务。由于GUI的复杂性，设计过程中的错误可能导致用户难以理解和操作，从而影响软件的使用体验和效率。因此，有效的验证方法对于减少错误和提高用户体验至关重要。这篇论文贡献了一种新的GUI对话框模型和验证策略，它克服了传统方法的局限性，提高了GUI软件验证的效率和准确性，对于GUI设计和开发领域具有重要的实践意义。

A Verification Method for Some GUI Dialogue Properties

Yoshihiro Tsujino

Division of Information and Production Science, Graduate School of Science and Technology,

Kyoto Institute of Technology, Kyoto, Japan 606-8585

SUMMARY

I propose a GUI dialogue model and an automatic

verification method in order to verify properties of reacha-

bility 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

Key words: GUI design; dialogue model; formal

specification; automatic verification; reachability problem.

1. Introduction

Today, creating good graphical user interface (GUI)

software is very difficult and expensive. For example, about

50% of the implementation cost of applications is devoted

to implementing the user interface portion [1]. Since it is

more difficult to design good GUI software than non-GUI

software, we should develop GUI software iteratively as

shown in Fig. 1 [16]. For building a prototype, we have

many support tools such as widget sets and tool kits [813].

On the other hand, for testing and/or evaluating prototypes,

we have few or no support tools because it is difficult to

check many GUI criteria automatically, such as usability

factors. But the size of application software and GUIs has

recently increased so it is inefficient to test all GUIs by

hand. It is especially difficult to verify reachability, that is,

the reachability from the initial state of GUI to the state in

which the specified command is executable, and unreacha-

bility, that is, the unreachability from the initial state to the

state in which no commands are executable (i.e., the dead-

lock state), since we must check all states in the GUI.

As a theoretical approach usable to verify user inter-

face properties automatically, methods in which a finite

state machine is the model of the dialogue between a user

and a system are known [3, 4]. Because the finite state

machine has only a finite number of states and we can check

all of its states and transitions, we can construct the verifi-

cation system theoretically. On the other hand, the finite

state machine model has some problems, as follows:

(1) Size of user interfaces

When the user interface is large, the corresponding

finite state machine has many states. Moreover, it has many

transitions at each state since the GUI has many input events

that can be accepted at the same time. Therefore, we cannot

verify GUI properties effectively in practice by checking all

Systems and Computers in Japan, Vol. 31, No. 14, 2000

Translated from Denshi Joho Tsushin Gakkai Ronbunshi, Vol. J82-D-I, No. 10, October 1999, pp. 12861294

Fig. 1. User interface development cycle.

下载后可阅读完整内容，剩余8页未读，立即下载

weixin_38626473

粉丝: 3
资源: 927

自动验证GUI对话框属性的方法

一些GUI对话属性的验证方法

Systemverilog for Verification

systemverilog_for_verification 源码

uvm clone

STM32 Utility

Encountered an SSL error. Most likely a certificate verification issue.

uvm refernce_model

htpps://sms-activate.org/

mitmdump 抓包错误：Certificate verification error for www.****.com: unable to get local issuer certificat...

最新资源