Practical Formal Methods in HCI

Alan Dix

HCI Centre, University of Birmingham, UK

Chapter in Computational Interaction. Antti Oulasvirta, Per Ola Kristensson, Xiaojun Bi, Andrew Howes (eds), Oxford University Press, 2018.

The use of precise formal methods at first seems in direct contradiction to the richness of human interaction.  However, this chapter argues that in fact formalism can be used effectively and practically in interaction design.

The term 'formal methods' in computer science refers to a suite of techniques drawing on mathematical notions of sets, logic and functions or precise diagrammatic notations.  Most current uses of these techniques are primarily focused on safety critical applications, such as aerospace or the nuclear industry, where the costs and expertise can be justified.  Indeed, many would regard research into broader use of these methods to be at best a theoretical interest.

However, historically, the development of formal methods in both general computer science and HCI was driven as much by practical considerations as theory, or perhaps more precisely, the early pioneers drew fewer distinctions between the two.

This chapter demonstrates through two case studies of real use how formal notations can be used in areas of practical interaction design (information systems and physical design) beyond the safety critical applications with which they are usually associated.  Furthermore, the examples show that appropriately designed notations can be understood, used, and appropriated by clients and designers who have no formal training or expertise. 

The two cases studies each offer specific notations and techniques that may be of use to the reader, but these are also used to explore the more general lessons for creating practical formal methods for HCI

Keywords: formal methods, physigram, information system design, physicality, physical computing, state-transition network, flowchart, dialogue modelling, product design, HCI, human–computer interaction.


Alan Dix 26/6/2017