- research topics
Formal methods in HCI
[books] [conferences] [selected
papers] [undo] [dialogue] [groups
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.
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.
full paper (PDF, 329K)
- Dix, A. J. (1991).
Formal methods for interactive systems. London: Academic Press.ISBN
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
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,
Looks at the entire design lifecycle, but dealing at some length with Fabio's
ConcurTaskTrees which combine hierarchical task analysis with Lotos concurrency
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
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
- 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.
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
- 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
- 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.
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.
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.
Research Groups and Projects
Various groups working on formal methods in HCI.
Please let me know about your group.
- The HCI Group at the University of York.
Where I started! Work on links to requirements engineering, formally specified 'interactors' and much else.
- The Human Computer Interaction Group at QMW College, University of London.
Another early player in the area. Special focus on task-based models.
- Interaction Design
Centre, Middlesex University
Work on formal user modelling applied particularly to small devices (PDAs, mobile phones). Also analysis of consumner devices and web pages using graph theoretic techniques.
- Computing Research Centre, Sheffield-Hallam University
Chris Roast (another ex-Yorkie) working with others on the formalisation of Green's 'cognitive dimensions' and other things.
Chris and Jawed Siddiqi are the driving force behind the FACHI workshops.
- College of
Computing, Georgia Tech.
Not a main topic, but Gregory Abowd's work includes using automated model checking for dialogue verification.
- Laboratoire d'Interaction Homme-Systémes, University of Toulouse.
If you want to know about Petri Nets - this is the place. Using object oriented extrensions to Petri Nets to model individual and collaborative systems.
- Human-Computer Interaction Group, CNUCE, Pisa.
What Toulouse is to Petri Nets, Pisa is to LOTOS!
Using LOTOS to specify 'interactors' (subtly different from York 'interactors') also linking goal-tree style task analysis to LOTOS specifications.
- Glasgow Accident Analysis Group, Glasgow University
Use formal notations amongst other non-formal appriaches to understand the causes of human error in accidents.
- MEFISTO EU funded project
Looking at applications in air traffic control. This involves partners from York, Toulouse, Pisa and elsewhere.
maintained by Alan Dix