The role of formal proof in modelling interactive behaviour

  • Richard Butterworth
  • Ann Blandford
  • David Duke
Part of the Eurographics book series (EUROGRAPH)


When proving properties of formally described interactive systems, trade-offs have to be made between the simplicity of the model — which relates to the ease of performing proofs — and the real-world validity of the model. This issue is particularly important when the proof incorporates properties of user behaviour as well as the device specification. This paper discusses these trade-offs, using a simple model of a web-browsing system as an example. The property we focus on relates to usability: showing whether or not the things a user wants to do are easy to do.

As well as adding detail to move from a point where the modelled system is simple but does not satisfy a stated usability property, through a model that satisfies the property but is ‘unreasonable’, to one that is both reasonable and usable, we also move from a ‘safety’-based proof to a ‘liveness’-based proof, arguing that although liveness proofs are generally more difficult to execute, they correspond better to our intuitive understanding of what it means for a system to be usable, and are therefore more valuable.


Interactive System Safety Property Usability Property Liveness Property Live Model 
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.
    B. Alpern and F. Schneider. Defining liveness. Information Processing Letters, 21:181–185, 1985.MathSciNetMATHCrossRefGoogle Scholar
  2. 2.
    D. Andrews and D. Ince. Practical formal methods with VDM. Series in software engineering. McGraw-Hill, 1991.Google Scholar
  3. 3.
    A. Blandford, R. Butterworth, and J. Good. Users as rational interacting agents: formalising assumptions about cognition and interaction. In Harrison and Torres [12], pages 43–60.Google Scholar
  4. 4.
    A. Blandford and R. Young. Specifying user knowledge for the design of interactive systems. Software Engineering Journal, pages 323–333, 1996.Google Scholar
  5. 5.
    R. Butterworth and A. Blandford. Programmable user models: the story so far. Technical report, Middlesex University, 1997. PUMA working paper WP8. Available from Scholar
  6. 6.
    R. Butterworth and D. J. Cooke. On biasing behaviour to the optimal. In Harrison and Torres [12], pages 291–306.Google Scholar
  7. 7.
    A. Dix. Formal Methods for Interactive Systems. Computers and People Series. Academic Press, 1991.Google Scholar
  8. 8.
    A. Dix and R. Mancini. Specifying history and back tracking mechanisms. In Formal methods in human-computer interaction, Formal approaches to computing and information technology, chapter 1, pages 1–23. Springer, 1998.Google Scholar
  9. 9.
    A. Hall. Seven myths of formal methods. IEEE Software, pages 11–19, September 1990.Google Scholar
  10. 10.
    M. Harrison and D. Duke. A review of formalisms for describing interactive behaviour. In R. Taylor and C. Coutaz, editors, Software engineering and human-computer interaction (Lecture notes in computer science vol. 896), pages 49–75. Springer Verlag, 1995.CrossRefGoogle Scholar
  11. 11.
    M. Harrison and H. Thimbleby, editors. Formal Methods in Human-Computer Interaction. Cambridge series on HCl. Cambridge University Press, 1990.MATHGoogle Scholar
  12. 12.
    M. Harrison and J. Torres, editors. Design, specification and verification of interactive systems ‘97. Eurographics, Springer, 1997.MATHGoogle Scholar
  13. 13.
    L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, 1994.CrossRefGoogle Scholar
  14. 14.
    C. Roast and J. Siddiqi, editors. Proceedings of the BCS-FACS Workshop on Formal Aspects of the Human Computer Interface. Springer Verlag, 1996. Proceedings published electronically at Scholar
  15. 15.
    J. Spivey. The Z Notation: A Reference Manual. Series in Computer Science. Prentice Hall International, 1989.MATHGoogle Scholar
  16. 16.
    B. Sufrin and J. He. Specification, analysis and refinement of interactive processes. In Harrison and Thimbleby [11], pages 153–199.Google Scholar
  17. 17.
    R. Young, T. Green, and T. Simon. Programmable user models for predictive evaluation of interface design. In K. Bice and C. Lewis, editors, Proceedings of CHI ‘89: Human Factors in Computing Systems, pages 15–19. Association of computing machinery, 1989.Google Scholar

Copyright information

© Springer-Verlag Wien 1998

Authors and Affiliations

  • Richard Butterworth
    • 1
  • Ann Blandford
    • 1
  • David Duke
    • 2
  1. 1.School of Computing ScienceMiddlesex UniversityLondonUK
  2. 2.Department of Computer ScienceUniversity of YorkYorkUK

Personalised recommendations