Pragmatic Formal Design: A Case Study in Integrating Formal Methods into the HCI Development Cycle

  • Meurig Sage
  • Chris Johnson
Conference paper
Part of the Eurographics book series (EUROGRAPH)


Formal modelling, in interactive system design, has received considerably less real use than might have been hoped. Formal methods can be expensive to use, with poor coverage of the design life cycle. In this paper, we suggest a pragmatic approach to formal design. We rely on a range of models that can help at different stages of development. We use as a case study, the design of a multi-user, design rationale editor. In the early stages of our design, we use a range of semi-formal notations, to perform a task analysis. We then develop a prototype in Clock, a high level functional language. From this, we derive a LOTOS specification, which we use to verify that our system satisfies important design requirements. The task analysis helps here, in highlighting these requirements. Throughout we rely on tool support to simplify the process, and so make it cost effective.


Model Check Design Rationale Tool Support Interactive System Task Analysis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    G Abowd and A Dix (1992), Giving undo attention. Interacting with Computers, 4(3):317–342.CrossRefGoogle Scholar
  2. 2.
    Heather Alexander (1990), Structuring dialogues using CSP, in MD Harrison and H Thimbleby, Formal methods in Human computer interaction, Cambridge University Press.Google Scholar
  3. 3.
    R Bentley (1994) Supporting multi-user interface development for cooperative systems, PhD thesis, Lancaster University.Google Scholar
  4. 4.
    I.M. Breedvelt-Schouten, F Paterno, C Severijns (1997) Reusable structures in task models, in MD Harrison, JC Torres (eds), Design, Specification and Verification of Interactive Systemsℙ97, Springer Computer Science, pp 225–241.Google Scholar
  5. 5.
    Judy Brown, T.C. Nicholas Graham and Timothy Wright (1998). The Vista Environment for the Coevolutionary Design of User Interfaces. In Proceedings of Human Factors in Computing Systems (CHI’98), ACM Press, Los Angeles, USA, April 1998 (to appear).Google Scholar
  6. 6.
    JC Campos, MD Harrison (1997), Formally verifying interactive systems: A review, in MD Harrison, JC Torres (eds), Design, Specification and Verification of Interactive Systemsℙ97, Springer Computer Science, pp 109–125.Google Scholar
  7. 7.
    Steven Clark (1997), Literate Development, PhD thesis, University of Glasgow.Google Scholar
  8. 8.
    J Conklin and ML Begeman (1989) gIBIS a tool for all reasons, in J. Amer. Soc. Info. Sci 200–213.Google Scholar
  9. 9.
    Joelle Coutaz (1997) PAC-ing the Architecture of Your Interface, in MD Harrison, JC Torres (eds), Design, Specification and Verification of Interactive Systems 97, Springer Computer Science, pp 13–29.Google Scholar
  10. 10.
    A. Dix and G. Abowd (1996) Modelling status and event behaviour of interactive systems, in Software Engineering Journal, 11(6) pp. 334–346.CrossRefGoogle Scholar
  11. 11.
    R Fields, N Merriam, A Dearden (1997) DMVIS: Design, modelling and validation of interactive systems, in MD Harrison, JC Torres (eds), Design, Specification and Verification of Interactive Systemsℙ97, Springer Computer Science, pp 29–45.Google Scholar
  12. 12.
    R Fields, N Merriam (1997) Modelling in Action. Reports from the DSVIS’97 working groups, in MD Harrison, JC Torres (eds), Design, Specification and Verification of Interactive Systemsℙ97, Springer Computer Science, pp307–320Google Scholar
  13. 13.
    Hubert Garavel (1996), An Overview of the Eucalyptus Toolbox. In Z Brezocnik and T Kapus, eds, Proceedings of the COST 247 Interactional Workshop on Applied Formal Methods in System Design (Maribar, Slovenia), pages 76–88. University of Maribor, Slovenia, June 1996.Google Scholar
  14. 14.
    T.C. Nicholas Graham and Tore Urnes (1996). Linguistic Support for the Evolutionary Design of Software Architectures. In Proceedings of the Eighteenth International Conference on Software Engineering. IEEE Computer Society Press, Berlin, Germany, pp. 418–427, March 1996.Google Scholar
  15. 15.
    T.C. Nicholas Graham, Herbert Damker, Catherine A. Morton, Eric Telford and Tore Urnes (1996). The Clock Methodology: Bridging the Gap Between User Interface Design and Implementation. York University Technical Report CS-96–04. York University, August 1996.Google Scholar
  16. 16.
    Phil Gray, David England and Steve McGowan (1994), XUAN: Enhancing the UAN to capture Temporal Relations among Actions, Technical Report IS-94–02, Department of Computing Science, University of Glasgow.Google Scholar
  17. 17.
    Thomas R Green (1989) Cognitive dimensions of notations. In A Sutcliffe and L Macaulay, eds, People and Computers IV, pages 443–460. Cambridge University Press, Cambridge, United Kingdom.Google Scholar
  18. 18.
    Saul Greenberg and David Marwood (1994), Real Time Groupware as a Distributed System: Concurrency Control and its Effect on the Interface, ACM 1994 Conference on Computer Supported Cooperative Work (CSCW’94), ACM SIGCHI & SIGOIS.Google Scholar
  19. 19.
    Michael D. Harrison and David J. Duke (1994), A review of formalisms for describing interactive behaviour, lecture notes in computer science 896, Software Engineering and Human-Computer Interaction, (ICSE’94 Workshop on SE-HCI).Google Scholar
  20. 20.
    H.R. Hartson, A.C. Siochi and D Hix (1990), The UAN: A User-Oriented Representation for Direct Manipulation Interface Designs. ACM Transactions on Information Systems, 8 (3) :pp191–203.CrossRefGoogle Scholar
  21. 21.
    Ralph Hill. (1992) The abstraction-link-view paradigm: Using constraints to connect user interfaces to applications. In ACM SIGCHI 1992, pages 335–342, April 1992.Google Scholar
  22. 22.
    CW Johnson (1996). Literate specifications, in Software Engineering Journal, July 1996, pp 225–237Google Scholar
  23. 23.
    CW Johnson (1997) Utility of User interface notations, submitted to the Journal of Human Computer Interaction, 1997.Google Scholar
  24. 24.
    P Johnson, S Wilson, P Markopoulos & J Pycock (1993) — ADEPT — Advanced design environment for prototyping with task models, Demonstration abstract. In Aschlund S et al (eds), Bridges Between Worlds- INTERCHIP, Addison-Wesley, pp 56.Google Scholar
  25. 25.
    Glen E Krasner and Stephen T Pope (1988), A cookbook for using the Model-View-Controller interface paradigm. Journal of Object-Oriented Programming, 1 (3):26–49.Google Scholar
  26. 26.
    A Maclean, R Young, V Bellotti, and T Moran (1996), Questions, Options and Criteria: Elements of Design Space Analysis, in Moran (1996).Google Scholar
  27. 27.
    Panos Markopoulos (1997), A compositional model for the formal specification of user interface software, PhD Thesis, QMW College, University of London.Google Scholar
  28. 28.
    TP Moran, JM Carroll (1996) (eds) Design Rationale: Concepts, techniques and use, Hillsdale, Lawrence Erlbaum Asoociates.Google Scholar
  29. 29.
    Brad A Myers, Dario A Giuse, Roger B Dannenberg, Brad Vander Zanden, David S Kosbie, Edward Pervin, Andrew Mickish and Philippe Marchal (1990), Garnet: Comprehensive Support for Graphical, Highly Interactive User Interfaces. In IEEE Computing, pages 71–85, Novermber 1990.Google Scholar
  30. 30.
    F Paterno and M Mezzanotte (1995), Formal verification of undesired behaviours in the CERD case study, in Proceedings of EHCI’95, Chapman & Hall Publisher.Google Scholar
  31. 31.
    S Pavon & D Larrabeiti (1993) LOLA (LOtos LAboratory) User Manual v3.4, Scholar
  32. 32.
    M Sage and CW Johnson (1997) Interactors and Haggis: Executable specifications for interactive systems, in MD Harrison, JC Torres (eds), Design, Specification and Verification of Interactive Systems 97, Springer Computer Science, pp 93–109.Google Scholar
  33. 33.
    S Shum (1991) Cognitive dimensions of design rationale. In D Diaper and N Hammond, eds, People and Computers VI: Proceedings of HCI’91. Cambridge University Press, Cambridge, United Kingdom.Google Scholar
  34. 34.
    S Shum (1993) QOC Design Rationale Retrieval: A Cognitive Task Analysis & Design Implications, Rank Xerox EuroPARC, Technical Report EPC-93–105Google Scholar
  35. 35.
    S Buckingham Shum (1996) Analyzing the Usability of a Design Rationale Notation, in Moran (1996).Google Scholar

Copyright information

© Springer-Verlag Wien 1998

Authors and Affiliations

  • Meurig Sage
    • 1
  • Chris Johnson
    • 1
  1. 1.GIST, Department of Computing ScienceUniversity of GlasgowGlasgowScotland, UK

Personalised recommendations