Formally-based tools for user interface analysis and design

Lead Research Organisation: Swansea University
Department Name: College of Science

Abstract

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.

Publications

10 25 50
publication icon
Harold N/a (2010) Reducing Number Entry Errors: Solving a Widespread, Serious Problem in J Royal Society Interface

publication icon
Harold Thimbleby (Co-Author) (2011) Buffer Automata: A UI architecture prioritising HCI concerns for interactive devices in THIS IS NOT A JOURNAL BUT RESEARCHFISH WONT ACCEPT IT WITHOUT A JOURNAL NAME

publication icon
Johnson TR (2013) SYFSA: a framework for systematic yet flexible systems analysis. in Journal of biomedical informatics

publication icon
Thimbleby H (2010) Reducing number entry errors: solving a widespread, serious problem. in Journal of the Royal Society, Interface

publication icon
Thimbleby H (2013) Action graphs and user performance analysis in International Journal of Human-Computer Studies

 
Description We showed that formal methods can be used very effectively in user interface design, particularly for safety-critical applications. We note that the user interface is often an 'add-on' and not subject to such careful design process that may be applied to other parts of a computer system. We found this applies particularly in medical systems. We developed many new techniques for improving the application of formal methods in user interface design.
Exploitation Route We have subsequently developed a formal methods tool based on PVS to animate and explore user interface designs.
Sectors Digital/Communication/Information Technologies (including Software),Healthcare