Model checking graphical user interfaces using abstractions
Matthew B. Dwyer, Vicki Carr, Laura Hines · ACM SIGSOFT Software Engineering Notes · 1997
Symbolic model checking techniques have been widely and successfully applied to statically analyze dynamic properties of hardware systems.Efforts to apply this same technology to the analysis of software systems has met with a number of obstacles, such as the existence of non-finite state-spaces.This paper investigates abstractions that make it possible to cost-effectively model check specifications of software for graphical user interface (GUI) systems.We identify useful abstractions for this domain and demonstrate that they can be incorporated into the analysis of a variety of systems with similar structural characteristics.The resulting domain-specific model cbecldug yields fast verification of naturally occurring specifications of intended GUI behavior.