Alan Dix - research topics

Formal methods in HCI

[general references][tutorials] [books] [conferences] [selected papers] [undo] [dialogue] [groups and projects]

This page is basically the annotated bibliography from my chapter in Monk and Gilbert (1995) and from Dix et al. (1998) with the odd extra bit. Please tell me about things that ought to be in here.

See also my other research topics pages, many of which involve some element of formal methods.

For wider formal methods research in computing see the formal methods pages of the WWW Virtual Library.

General

A. Dix, J. Finlay, G. Abowd and R. Beale (1998/1993).
Chapters 8 and 9, Human-Computer Interaction.
Prentice Hall. second edition

• Monk, A. F. and Gilbert, N., editors , (1995).
  Perspectives on HCI: Diverse Approaches. London, Academic Press.
  A collection of articles introducing key areas of HCI, including formal models (Chapter 2) and formal specification (Chapter 3). Readable introductions for newcomers to these topics.
  abstract and introduction | full paper (PDF, 329K)

Tutorials

• From Formalism to Physicality
  masterclass at  UPC North: Understanding People and Computers, 30th April 2008.
• Effective Use of Formal Methods in Interface Specification
  The pages for my HCI'96 tutorial in London.
  Includes an online copy of the notes and exercises (PDF).

Books

• Dix, A. J. (1991).
  Formal methods for interactive systems. London: Academic Press.ISBN 0-12-218315-0
  This covers the PIE model and many extensions and other models, including those on which status/event analysis is based.
  table of contents
• Harrison, M.D. and Thimbleby, H.W., editors (1990).
  Formal Methods in Human Computer Interaction. Cambridge: Cambridge University Press.
  An edited collection covering a range of formal techniques.
• Palanque, P. and Paterno,F., editors (1997).
  Formal Methods in Human Computer Interaction. London, Springer-Verlag.
  Just to confuse you! Another more recent edited collection. Each chapter takes a different technique or notation and uses it to specify the same example, a web browser.
• Paterno,F. (2000).
  Model-Based Design and Evaluation of Interactive Applications. London, Springer-Verlag.
  Looks at the entire design lifecycle, but dealing at some length with Fabio's ConcurTaskTrees which combine hierarchical task analysis with Lotos concurrency operators. Fabio's web pages for the book
• Thimbleby, H. W. (1990).
  User Interface Design. New York: ACM Press, Addison-Wesley.
  A wide ranging book which some extensive explicit formal material, and employing a formal approach to problems in much of its informal material.

Conferences and Journals

• C. Roast and J. Siddiqi (eds), (1996).
  FAHCI - Formal Aspects of the Human Computer Interface, Springer Verlag,
  Report of a workshop of the same name held in 1996, principally containing articles on formal specification and modelling, but also includes some cognitive modelling.
  FAHCI98, was held in Sheffield in September 1998. Some papers from it are being published in several places.
• There is an annual conference held under the auspices of Eurographics, called 'Design Specification and Verification of Interactive Systems'.
  The proceedings of each conference, DSVIS'94 - DSVIS'01, are published by Springer.
• Engineering Human Computer Interaction
  Triennial working conference of IFIP Working Group 2.7 (13.4), the next is EHCI01 in May 2001 in Toronto
  Usually includes various papers on formal methods in HCI.
• Formal Methods Elsewhere - FME2000
  A new workshop focused on 'different' uses of formal methods, which includes many HCI-related applications. It is likely to become an annual event attached to different larger conferences.
  Full proceedings available as volume 43 of Elsevier's Electronic Notes in Theoretical Computer Science
• Interacting with Computers Volume 9, Issue 2, 3 Nov. 1997, Special Issue on Formal Aspects of Human Computer Interaction

Selected papers

• Dix, A. J. and Runciman, C. (1985)
  Abstract models of interactive systems.
  In HCI'85: People and Computers I: Designing the Interface, Johnson, P. and Cook, S. (eds.), pp. 13-22. Cambridge: Cambridge University Press.
  The original PIE paper! [full paper online]
  
• Sufrin, B. (1982)
  Formal specification of a display editor.
  Science of Computer Programming, 1, 157-202
  A classic paper describing the formal specification of a display based text editor.
• Dix, A. J. (1992).
  Beyond the interface.
  In Engineering for Human-Computer Interaction, Larson, J. and Unger, C. (eds.), pp. 171-190. North-Holland.
  Describes some aspects of status/event analysis relating status/event phenomena to the timescales over which they operate and the concept of pace. See also Chapter 9 of (Dix et al., 1993) for status-event timeline diagrams and Chapter 10 of (Dix, 1991) for its formal roots.

Undo

Formal methods have been particularly useful in addressing issues of undo. Here are a few papers to read. In addition, see Chapter 2 and 4 of (Dix, 1991) and Chapter 12 of (Thimbleby, 1990) and my topics page on undo.

• Abowd, G. D. and Dix, A. J. (1992).
  Giving undo attention.
  Interacting with Computers, 4(3), 317-342.
  A formal analysis of undo in the context of group editing.
  abstract || full paper (compressed postscript, 112K) || full paper (PDF, 284K)
  
• Archer, Jr., J., Conway, R. and Schneider, F.B. (1984)
  User recovery and reversal in interactive systems.
  ACM Transactions on Programming Languages, 6(1), pp. 1-19.
  A classic paper analysing different forms of undo.
• Vitter, J. S. (1984).
  US&R: A new framework for redoing.
  IEEE Software, 1(4), pp. 39-52.
  Takes undo and redo to its extreme!
• Yang, Y. (1988). Undo support models.
  International Journal of Man-Machine Studies, 28(5), pp. 457-481.
  Informal analysis and review.

Dialogue

As well as the following, see Chapter 8 of (Dix et al., 1993) which describes dialogue properties in more detail and any book on UIMS.

• Alexander, H. (1987)
  Formally-based Tools and Techniques for Human-Computer Dialogues. London: Ellis Horwood.
  Describes her SPI notation which is both quite powerful and very easy to read.
• Thimbleby, H.W. (1993).
  Combining systems and manuals.
  In HCI'93: People and Computers VIII, J.L. Alty, D. Diaper and S. Guest (Eds.) pp. 479-488. Cambridge: Cambridge University Press.
  Describes the Hyperdoc tool, which supports simulation, dialogue analysis and automatic documentation.