Skip to main content
SpringerLink
Log in

Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors

  • Conference paper
Integrated Formal Methods (IFM 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2999))

Included in the following conference series:

Abstract

Interactive systems combine a human operator with a computer. Either may be a source of error. The verification processes used must ensure both the correctness of the computer component, and also minimize the risk of human error. Human-centred design aims to do this by designing systems in a way that make allowance for human frailty. One approach to such design is to adhere to design rules. Design rules, however, are often ad hoc. We examine how a formal cognitive model, encapsulating results from the cognitive sciences, can be used to justify such design rules in a way that integrates their use with existing formal hardware verification techniques. We consider here the verification of a design rule intended to prevent a commonly occurring class of human error know as the post-completion error.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Back, R., Mikhajlova, A., von Wright, J.: Modeling component environments and interactive programs using iterative choice. Technical Report 200, Turku Centre for Computer Science (September 1998)

    Google Scholar 

  2. Blandford, A.E., Young, R.M.: The role of communication goals in interaction. In: Adjunct Proceedings of HCI 1998, pp. 14–15 (1998)

    Google Scholar 

  3. Blandford, A.E., Barnard, P.J., Harrison, M.D.: Using interaction framework to guide the design of interactive systems. International Journal of Human Computer Studies 43, 101–130 (1995)

    Article  Google Scholar 

  4. Blandford, A.E., Butterworth, R., Curzon, P.: PUMA footprints: linking theory and craftskill in usability evaluation. In: Proc. of Interact, pp. 577–584 (2001)

    Google Scholar 

  5. Bumbulis, P., Alencar, P.S.C., Cowen, D.D., Lucena, C.J.P.: Validating properties of component-based graphical user interfaces. In: Bodart, F., van der Donckt, J. (eds.) Proc. Design, Specification and Verification of Interactive Systems 1996, pp. 347–365. Springer, Heidelberg (1996)

    Google Scholar 

  6. Butterworth, R., Blandford, A.E., Duke, D.: Using formal models to explore display based usability issues. Journal of Visual Languages and Computing 10, 455–479 (1999)

    Article  Google Scholar 

  7. Butterworth, R., Blandford, A.E., Duke, D.: Demonstrating the cognitive plausibility of interactive systems. Formal Aspects of Computing 12, 237–259 (2000)

    Article  MATH  Google Scholar 

  8. Byrne, M., Bovair, S.: A working memory model of a common procedural error. Cognitive Science 21(1), 31–61 (1997)

    Article  Google Scholar 

  9. Campos, J.C., Harrison, M.D.: Formally verifying interactive systems: a review. In: Harrison, M.D., Torres, J.C. (eds.) Design, Specification and Verification of Interactive Systems 1997, pp. 109–124. Springer, Wien (1997)

    Google Scholar 

  10. Curzon, P., Blandford, A.E.: Using a verification system to reason about postcompletion errors. Presented at Design, Specification and Verification of Interactive Systems (2000), Available from http://www.cs.mdx.ac.uk/puma/asWP31

  11. Curzon, P., Blandford, A.E.: Detecting multiple classes of user errors. In: Nigay, L., Little, M.R. (eds.) EHCI 2001. LNCS, vol. 2254, pp. 57–71. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  12. Curzon, P., Blandford, A.E.: From a formal user model to design rules. In: Forbrig, P., Limbourg, Q., Urban, B., Vanderdonckt, J. (eds.) DSV-IS 2002. LNCS, vol. 2545, pp. 19–33. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Duke, D.J., Barnard, P.J., Duce, D.A., May, J.: Syndetic modelling. Human-Computer Interaction 13(4), 337–394 (1998)

    Article  Google Scholar 

  14. Fields, R.E.: Analysis of erroneous actions in the design of critical systems. Technical Report YCST 20001/09, University of York, Department of Computer Science, D.Phil Thesis (2001)

    Google Scholar 

  15. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  16. Gray, W., Young, R.M., Kirschenbaum, S.: Introduction to this special issue on cognitive architectures and human-computer interaction. Human-Computer Interaction 12, 301–309 (1997)

    Article  Google Scholar 

  17. Gray, W.D.: The nature and processing of errors in interactive behavior. Cognitive Science 24(2), 205–248 (2000)

    Article  Google Scholar 

  18. Hollnagel, E.: Cognitive Reliability and Error Analysis Method. Elsevier, Amsterdam (1998)

    Google Scholar 

  19. Kieras, D.E., Wood, S.D., Meyer, D.E.: Predictive engineering models based on the EPIC architecture for a multimodal high-performance human-computer interaction task. ACM Trans. Computer-Human Interaction 4(3), 230–275 (1997)

    Article  Google Scholar 

  20. Leadbetter, D., Lindsay, P., Hussey, A., Neal, A., Humphreys, M.: Towards model based prediction of human error rates in interactive systems. In: Australian Comp. Sci. Communications: Australasian User Interface Conf., vol. 23(5), pp. 42–49 (2001)

    Google Scholar 

  21. Moher, T.G., Dirda, V.: Revising mental models to accommodate expectation failures in human-computer dialogues. In: Design, Specification and Verification of Interactive Systems 1995, pp. 76–92. Springer, Wien (1995)

    Google Scholar 

  22. Paterno’, F., Mezzanotte, M.: Formal analysis of user and system interactions in the CERD case study. In: Proceedings of EHCI 1995: IFIP Working Conference on Engineering for Human-Computer Interaction, pp. 213–226. Chapman and Hall Publisher, Boca Raton (1995)

    Google Scholar 

  23. Ritter, F.E., Young, R.M.: Embodied models as simulated users: introduction to this special issue on using cognitive models to improve interface design. Int. J. Human-Computer Studies 55, 1–14 (2001)

    Article  MATH  Google Scholar 

  24. Roast, C.R.: Modelling unwarranted commitment in information artifacts. In: Chatty, S., Dewan, P. (eds.) Engineering for Human-Computer Interaction, pp. 77–90. Kluwer Academic Press, Dordrecht (1998)

    Google Scholar 

  25. Rushby, J.: Using model checking to help discover mode confusions and other automation suprises. In: 3rd Workshop on Human Error, Safety and System Development, HESSD 1999 (1999)

    Google Scholar 

  26. Xiong, H., Curzon, P., Tahar, S., Blandford, A.: Formally linking MDG and HOL based on a verified MDG system. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 205–224. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Interaction Design Centre, Middlesex University, Bramley Road, London, N14 4YZ

    Paul Curzon

  2. University College London Interaction Centre, Remax House, 31-32 Alfred Place, London, WC1E 7DP

    Ann Blandford

Authors
  1. Paul Curzon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ann Blandford
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK

    Eerke A. Boiten

  2. Department of Computing, University of Sheffield, S1 4DP, Sheffield, UK

    John Derrick

  3. School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Australia

    Graeme Smith

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Curzon, P., Blandford, A. (2004). Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24756-2_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21377-2

  • Online ISBN: 978-3-540-24756-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation