Skip to main content
SpringerLink
Log in

From formal models to formal methods

  • Submitted Papers
  • Conference paper
  • First Online:
Software Engineering and Human-Computer Interaction (SE-HCI 1994)

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

Included in the following conference series:

Abstract

Despite apparent success in using formal models to capture principles of human-system interaction, there are few accounts that consider how these results might be applied in practical software development. This paper is based on work conducted within an ESPRIT Basic Research Action (Amodeus-2) investigating means of design expression and transfer. Within Amodeus we are applying formal methods to the analysis of large design spaces. The focus of this paper is on some initial results obtained from the specification of an interactive system for managing audio-visual (AV) connections in an office environment. Our concern is how the specification (and formal methods in general) can be used to address design issues that impact the user interface. We argue that although formal models cannot guarantee that a system will be ‘usable’, they provide a precise design representation which can be tempered and informed by other perspectives.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Abowd. Formal aspects of human-computer interaction. D.Phil Thesis, Oxford University Computing Laboratory: Programming Research Group, 1991. Available as Technical Monograph PRG-97.

    Google Scholar 

  2. S. Bly, S. Harrison, and S. Irwin. Media spaces: Bringing people together in a video, audio and computing environment. Communications of the ACM, 36(1), January 1993.

    Google Scholar 

  3. P. Dourish and S. Bly. Portholes: Supporting awareness in distributed work groups. In Proc. ACM Conference on Human Factors in Computer Systems: CHI '92. Addison-Wesley. 1992.

    Google Scholar 

  4. D.J. Duke, G. Faconti, M.D. Harrison, and F. Paterno'. Unifying views of interactors. In Proc International Workshop on Advanced Visual Interfaces, 1994. To appear.

    Google Scholar 

  5. D.J. Duke and M.D. Harrison. Abstract interaction objects. Computer Graphics Forum, 12(3), 1993. Conference Issue: Proc. Eurographics'93.

    Google Scholar 

  6. D.J. Duke and M.D. Harrison. Mapping user requirements to implementations. To appear in Software Engineering Journal. Based on Amodeus-2 document sysmod/sm_wpl6, 1993.

    Google Scholar 

  7. D.J. Duke and M.D. Harrison. Connections: From A(V) to Z. Technical Report SM/WP29, ESPRIT BRA 7040 Amodeus-2, January 1994. File: sysmod/sm_wp29.ps.

    Google Scholar 

  8. D.J. Duke and M.D. Harrison. FSM analysis of access control. Technical Report SM/WP42, ESPRIT BRA 7040 Amodeus-2, October 1994.

    Google Scholar 

  9. D.J. Duke and M.D. Harrison. A preliminary FSM analysis of the CERD. Technical Report SM/IR8, ESPRIT BRA 7040 Amodeus-2, May 1994.

    Google Scholar 

  10. B. Gaver, T. Moran, A. MacLean, L. Lovstrand, P. Dourish, K. Carter, and B. Buxton. Realising a video environment: Europarc's RAVE system. In Proc. ACM Conference on Human Factors in Computer Systems: CHI '92. Addison-Wesley, 1992.

    Google Scholar 

  11. A. Hall. Seven myths of formal methods. Software, pages 11–19, September 1990.

    Google Scholar 

  12. M.D. Harrison. A model for the option space of interactive systems. In Engineering for Human-Computer Interaction: Proc IFIP WG2.7 Conf. Elsevier, 1992.

    Google Scholar 

  13. M.D. Harrison and A. Dix. A state model of direct manipulation. In M.D. Harrison and H.W. Thimbleby, editors, Formal Methods in Human Computer Interaction, pages 129–151. Cambridge University Press, 1990.

    Google Scholar 

  14. M.D. Harrison, C.R. Roast, and P.C. Wright. Complementary methods for the iterative design of interactive systems. In G. Salvendy and M. Smith, editors, Designing and Using Human-Computer Interfaces and Knowledge Based Systems. Elsevier Scientific, 1989.

    Google Scholar 

  15. C.W. Johnson and M.D. Harrison. Using temporal logic to support the specification and prototyping of interactive control systems. Int. J. Man-Machine Studies, 37:357–385, 1992.

    Google Scholar 

  16. C.B. Jones. Systematic Software Development Using VDM. Prentice Hall International, second edition, 1990.

    Google Scholar 

  17. L.S. Marshall. Formally describing interactive systems. In C.B. Jones and R. Shaw, editors, Case Studies in Systematic Software Development, pages 293–336. Prentice Hall, 1990.

    Google Scholar 

  18. F. Paterno and G. Faconti. On the use of LOTOS to describe graphical interaction. In A. Monk, D. Diaper, and M. Harrison, editors, People and Computers VII: Proc. of the HCI'92 Conference, Conference Series, pages 155–173. British Computer Society, 1992.

    Google Scholar 

  19. B. Sufrin and J. He. Specification, refinement, and analysis of interactive processes. In M.D. Harrison and H.W. Thimbleby, editors, Formal Methods in Human Computer Interaction, pages 153–200. Cambridge University Press, 1990.

    Google Scholar 

  20. J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International, second edition, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, University of York, YO1 5DD, Heslington, York, UK

    D. J. Duke & M. D. Harrison

Authors
  1. D. J. Duke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. D. Harrison
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Richard N. Taylor Joëlle Coutaz

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Duke, D.J., Harrison, M.D. (1995). From formal models to formal methods. In: Taylor, R.N., Coutaz, J. (eds) Software Engineering and Human-Computer Interaction. SE-HCI 1994. Lecture Notes in Computer Science, vol 896. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035813

Download citation

  • DOI: https://doi.org/10.1007/BFb0035813

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59008-8

  • Online ISBN: 978-3-540-49173-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation