The use of formal models for user interface design can provide a number of benefits. It can help to ensure consistency across designs for multiple platforms, prove properties such as reachability and completeness, and, perhaps most importantly, can help incorporate the user interface design process into a larger, formally-based, software development process. Often, descriptions of such models and examples are presented in isolation from real-world practice in order to focus on particular benefits, small focused examples, or the general methodology. This paper presents a case study of developing the user interface to a new software application using a particular pair of formal models, presentation models, and presentation interaction models. The aim of this study was to practically apply the use of formal models to the design process of a UI for a new software application. We wanted to determine how easy it would be to integrate such models into our usual development process and to find out what the benefits, and difficulties, of using such models were. We will show how we used the formal models within a user-centered design process, discuss what effect they had on this process, and explain what benefits we perceived from their use. We approach software design with the intention of building correct, robust, usable systems.

This means that for the functionality of our software we use formal methods, such as developing a specification in a formal language. We began by discussing these requirements with potential users of the system. Typically in a UI development process, we may have several such “brain-storming” sessions with different groups of users, using such things as post-it notes and whiteboards to ensure a collaborative and interactive discussion process. Following this, we then identified the key user requirements and started to consider how the functional requirements of the system should be represented as user requirements within the UI. Information stored in the application should reflect the hierarchical and component-based nature of the models. It should, therefore, allow for declarations to be entered and stored independently from completed models and used as required. Similarly, the described presentation models should exist as both detailed, complete models in their own right as well as components within conjunctions to build up other models. It should, in this manner and also all other respects, follow the syntax and semantics given.