Including Design Guidelines in the Formal Specification of Interfaces in Z

  • Judy Bowen
  • Steve Reeves
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


For any sort of computer system, the problems of being sure you have asked for the right thing and then being sure you are implementing the right thing are important and hard problems. For systems with a graphical user interface there are the analogous additional problems of making sure that the interface allows any interaction that is required, and works in a usable way. Design guidelines are used in both the design and evaluation of user interfaces to try and ensure that the systems we build are both usable and conform to specific requirements. This paper discusses practical ways in which we can use formal methods to model guidelines for interface design and then use these as a basis for the formal proof that a specified system has the desired properties described in the guidelines.


Graphical User Interface Formal Method Interface Design Design Guideline Selection Control 
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.
  2. 2.
    GNOME Human Interface Guidelines (1.0) (2002), available at,
  3. 3.
    Isys Information Architects Inc., Interface Hall of Shame,
  4. 4.
    Bodard, F., Hennebert, A., Leheureux, J., Vanderdonckt, J.: Towards a Dynamic Strategy for Computer-Aided Visual Placement. In: Catarci, T., Costabile, M., Levialdi, S., Santucci, G. (eds.) Proceedings of Advanced Visual Interfaces, pp. 78–87 (1994)Google Scholar
  5. 5.
    Bowen, J.: Formal Specification and Documentation Using Z. A Case Study Approach. International Thomson Computer Press (1996)Google Scholar
  6. 6.
    Dix, A., Runciman, C.: Abstract models of interactive systems. In: Jonhson, P., Cook, S. (eds.) People and Computers: Designing the Interface, pp. 13–22. Cambridge University Press, Cambridge (1985)Google Scholar
  7. 7.
    Dix, A., Finlay, J., Abowd, G., Beale, R.: Human-Computer Interaction, 2nd edn. Prentice Hall Europe, Englewood Cliffs (1997)Google Scholar
  8. 8.
    Duke, D., Harrison, M.: Abstract Interaction Objects. Computer Graphics Forum 12(3), C-25–C-26 (1993)Google Scholar
  9. 9.
    Duke, D., Harrison, M.: Interaction and task requirements. In: Palanque, P., Bastide, R. (eds.) DSV-IS 1995: Eurographics Workshop on Design, Specification and Verification of Interactive Systems, pp. 54–75. Springer, Heidelberg (1995)Google Scholar
  10. 10.
    Harrison, M., Dix, A.: A state model of direct manipulation in interactive systems. In: Harrison, M., Thimbleby, H. (eds.) Formal Methods in Human-Computer Interaction. Cambridge University Press, Cambridge (1990)Google Scholar
  11. 11.
    Horrocks, I.: Constructing the User Interface with Statecharts. Addison-Wesley, Reading (1999)Google Scholar
  12. 12.
    Jacky, J.: The Way of Z: Practical programming with formal methods. Cambridge University Press, Cambridge (1997)Google Scholar
  13. 13.
    Jacquot, J.-P., Quesnot, D.: Early Specification of User-Interfaces: Toward a Formal Approach. In: Proceedings of the 19th International Conference on Software Engineering, pp. 150–160. ACM Press, New York (1997)Google Scholar
  14. 14.
    Knight, J., Brilliant, S.: Premliminary Evaluation of a Formal Approach to User Interface Specification. In: Proceedings of the 10th International Conference of Z Users on the Z Formal Specification Notation, pp. 329–346 (1997)Google Scholar
  15. 15.
    Lok, S., Feiner, S., Nga, G.: Evaluation of Visual Balance for Automated Layout. In: Proceedings of the 9th International Conference on Intelligent User Interface. ACM Press, New York (2004)Google Scholar
  16. 16.
    Took, R.: Putting Design into Practice: Formal Specification and the User Interface. In: Harrison, M., Thimbleby, H. (eds.) Formal Methods in Human-Computer Interaction. Cambridge University Press, Cambridge (1990)Google Scholar
  17. 17.
    Saaltink, M.: The Z/EVES System. In: Bowen, J., Hinchey, M., Till, D. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72–88. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  18. 18.
    Smith, S., Mosier, J.: Guidelines for designing user interface software. Report EDS-TR86 -278. The MITRE Corporation, Bedford (1986)Google Scholar
  19. 19.
    Stepney, S., Polack, F., Toyn, I.: An outline pattern language for Z. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 2–19. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  20. 20.
    Stepney, S., Polack, F., Toyn, I.: A Z patterns catalogue I: specification and refactoring, v0.1. Technical Report YCS-2003-349, York (2003)Google Scholar
  21. 21.
    Sufrin, B., He, J.: Specification, analysis and refinement of interactive processes. In: Harrison, M., Thimbleby, H. (eds.) Formal Methods in Human-Computer Interaction. Cambridge University Press, Cambridge (1990)Google Scholar
  22. 22.
    Systä, K.: Adding user interface to a behavioral specification. In: Engineering for Human-Computer Interaction, pp. 227–244. Chapman and Hall, Boca Raton (1995)Google Scholar
  23. 23.
    Thimbleby, H.: User interface design with matrix algebra. ACM transactions, Computer-Human Interaction 11(2), 181–236 (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Judy Bowen
    • 1
  • Steve Reeves
    • 1
  1. 1.Department of Computer ScienceUniversity of WaikatoNew Zealand

Personalised recommendations