With the development of human-computer interactive technology, the interface between computers and users is more and more natural, the management of user interface is becoming more and more complex. Now, the available models of next generation user interface are almost conceptual. The formal specification and property verification to them are necessary. Based on the results of the research on natural interactive user interface, the authors give out a general model of interactive user interface. In order to guarantee the correction of the design of system, it needs to specify and verify it rigidly. The formal description and verification by use of LOTOS (language of temporal ordering specification) and ACTL (action based temporal logic) are given out in this paper. These allow people to study, evaluate and define the dynamic behavior of current user interfaces.