From formal models to formal methods

  • D. J. Duke
  • M. D. Harrison
Submitted Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 896)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Abo91]
    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. [BHI93]
    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. [DB92]
    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. [DFHP94]
    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. [DH93a]
    D.J. Duke and M.D. Harrison. Abstract interaction objects. Computer Graphics Forum, 12(3), 1993. Conference Issue: Proc. Eurographics'93.Google Scholar
  6. [DH93b]
    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. [DH94a]
    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/ Scholar
  8. [DH94b]
    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. [DH94c]
    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. [GMM+92]
    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. [Hal90]
    A. Hall. Seven myths of formal methods. Software, pages 11–19, September 1990.Google Scholar
  12. [Har92]
    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. [HD90]
    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. [HRW89]
    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. [JH92]
    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. [Jon90]
    C.B. Jones. Systematic Software Development Using VDM. Prentice Hall International, second edition, 1990.Google Scholar
  17. [Mar90]
    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. [PF92]
    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. [SH90]
    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. [Spi92]
    J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International, second edition, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • D. J. Duke
    • 1
  • M. D. Harrison
    • 1
  1. 1.Dept. of Computer ScienceUniversity of YorkHeslington, YorkUK

Personalised recommendations