Formal Models and Refinement for Graphical User Interface Design

Formal approaches to software development require that we correctly describe (or specify) systems in order to prove properties about our proposed solution prior to building it. We must then follow a rigorous process to transform our specification into an implementation to ensure that the properties we have proved are retained. When we design and build the user interfaces of our systems we are similarly keen to ensure that they have certain properties before we build them. For example, do they satisfy the requirements of the user? Are they designed with known good design principles and usability considerations in mind? User-centred design approaches, which incorporate many different techniques which we may consider as informal, seek to consider these issues so that the UIs we build are designed around the needs and capabilities of real users. Both formal methods and user-centred design are important and beneficial in the development of underlying system functionality and user interfaces respectively. Given this we would like to be able to use both approaches in one integrated software development process. Their differences, however, make this a challenging objective. In this thesis we present a solution this problem by describing models and techniques which provide a bridge between the existing work of user-centred design practitioners and formal methods practitioners enabling us to incorporate (representations of) informal design artefacts into a formal software development process. We then use these models as the basis for a refinement theory for user interfaces which allows interface designers to retain their informal design methods whilst providing an underlying theory grounded in the trace refinement theory of the Microcharts language