This chapter explores how precise formal methods 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 of which are currently primarily focused on safety-critical applications in the aerospace or nuclear industries. While research into broader use of these methods could be regarded as a theoretical interest, the early development of formal methods was driven as much by practical considerations as theory. This chapter features two case studies on formal notations and their use in areas of practical interaction design beyond safety-critical applications, as well as understood, used, and appropriated by clients and designers who have no formal training or expertise. Each offers specific notations and techniques to the reader and also explores more general lessons for creating practical formal methods for HCI.
iChoice: Applied value-sensitive human-computer interaction design