Towards a Formal Integrated Model for Function and User Interface

Interactive application has been developed rapidly around the world, especially in mobile devices and web applications. There is a need for further integration of research in software engineering and human-computer interaction. Object-Z is used to specify functional requirements whereas task models are employed to modeling UI requirements. The lack of integration of these two related models may introduce redundancies and inconsistencies into the software development process. In this paper, we propose an integrated model, consisting of functional models and task models, for capturing functional and UI requirements. Object-Z is used to capture formal functional requirements and Concur Task Trees is employed to specify the detailed user interactions. Both models are used in a complementary manner and are formally related through input/output variables and nodes of CTT tree. The formal semantics of the integrated model is given with extended finite state automata.