Formally-based tools for user interface analysis and design

Computers have become an integral part of modern society, from the desktop machines that people use at home, work or school, to the computers hidden inside mobile phones, DVD players and ticket machines. People now have to interact with complex machines more often than ever before, and although they can bring great advantages, we all have had bad experiences where the interaction doesn't turn out the way we wanted or expected. Such problems can be annoying (e.g., making a mistake whilst texting someone), serious breakdowns (people who can't use their car at all because the burglar alarm won't disarm), and in the worst cases lead to loss of life (when complex interactive devices are used in hospitals for patient care), financial and other mission critical problems.HCI has studied interface issues for many years, and has had particular success in understanding the 'before and after' of interface design. User requirements gathered beforehand inform design. After a system has been specified it can be evaluated (as a prototype or as a working program), and design iterated. However, HCI has had less impact on programmers and core programming decisions: the language of HCI is not often expressed in programming terms, such as invariants. Our research will focus on this issue, an area of high leverage, particularly for safety critical and dependable interactive systems which must be formally specified if their properties are to be ensured. Empowering programmers to adopt certain HCI principles will help ensure systems are more amenable to HCI-driven iterative design, and hence are more usable - whether by being easier to improve or starting off being better .There is a long tradition in formal HCI of using mathematics to describe the user interface, along with other aspects of 'the system', such as the user. Building on this tradition, we have already shown how a mathematical model of a interface can be used to identify inconsistencies in the design, which are liable to catch users out. Our research will develop and generalise similar techniques, to describe common notions of good interface design, such as simplicity and consistency, in useful mathematical models.Our research will embed the theory in analysis and evaluation tools, so it can be applied to real device designs. This will make the theory base available both to designers and to researchers. A libary of device designs will be built, which will both help demonstrate the tool and its underlying theory and their benefits, as well as allow researchers to experiment with and validate the theories on a variety of devices and scenarios. The library will also support other approaches; it is intended to be of far wider scope and benefit than this project alone.The tool will be developed using best practice, conforming to open international standards as appropriate so that it can be very widely used.