Human-computer interaction (HCI), as a discipline, is overwhelmingly experimental. One quick look at the proceedings of CHI [1,2], the leading conference in the domain, will make this clear: almost all papers report on carefully crafted, well-designed experiments. But what about the design of user interfaces for safety-critical systems, for example? Such systems as a whole require a high level of assurance, which is usually obtained via the use of formal methods. Rather than being founded on experiments and statistics, formal methods rely on other parts of mathematics (both continuous and discrete) to obtain guarantees rather than statistical confidence.

And this is where this book fits: the intersection of HCI and formal methods. Rather than (human) experiments, this domain is driven by models and case studies. This “handbook” is very much a snapshot in time, capturing the state of the domain. This is an explicit design decision of the editors, and it is carefully maintained throughout the book, both in the arrangement of the chapters and in the choice of chapters. It seems to give an excellent introduction to the literature. To their credit, the authors of the many chapters give an account of each topic by acknowledging the full history of the domain, rather than concentrating only on the latest fads. There is quite a bit of overlap here with work done in human factors, but the tools brought to bear are those found in software engineering.

The book is divided into four parts: “Introduction”; “Modeling, Execution and Simulation”; “Analysis, Validation and Verification”; and “Future Opportunities and Developments.” Each part contains four to six chapters. The introductory chapters cover the state of the art, topics, trends and gaps, and case studies of formal methods in HCI as a domain of study. These are written by teams led by the editors of the book, who also seem to be senior members of the community. I was particularly impressed by the care taken in the first part, the introduction chapters. These summative chapters require a tremendous amount of work to write but do not earn their authors much academic credit.

The writing is uniformly crisp. Each chapter is self-contained and covers a well-defined topic. There are some odd minor flaws: for several chapters, the addresses of the “authors” are not actually of the authors of that chapter! Furthermore, in more than one paper, authors use full words as identifiers in mathematical expressions in LaTeX math mode, which is a basic typesetting error (which hinders the readability of the results; for a book, readability is a fundamental usability concern--and yet the authors are supposed to be HCI experts!). One can feel the influence of formal methods adherents quite strongly throughout this book, and it does not read like an HCI methods book, such as MacKenzie’s excellent book [3].

I enjoyed reading the book and will recommend several of the chapters to some of my graduate students. As reference material, this handbook is great; I would definitely recommend it to anyone who needs that. It does not seem like there is (yet) a textbook of formal methods in HCI. While I would not actively recommend this book as an entry point into the domain, until there is such a textbook, it can act as a reasonable proxy.