Satisfiability-based checking for user interface model

The design of user interface is closely related with system quality and usability. Many researches have been done on user interface testing method, test case generation and user interface model syntax checking, but less have been done on state attribute checking of user interface model. Because model state space is large and dynamic, this kind of checking of user interface is difficult. This article introduces the user interface model, presents encoding transform from user interface model to proposition formula. Then we encode the proposition formula and the checked attribute, translate into satisfiability instance, and input the instance into satisfiability tools for solve. The problem of state attribute checking of user interface model becomes the satisfiability of the proposition formula. We illustrate an example to demonstrate the validity of our checking method for user interface model.