In this paper, we propose to base the verification of a GUI application on a reference model used in
. The reference model is a formal model for the behavior of the GUI application. It is derived by dynamic analysis (hence “black-box”). Thus, it can be used to account for the graphical interface even when the GUI toolkit is not amenable to formal analysis or its source code is not available. We have implemented our approach; a preliminary case study indicates its feasibility in principle.