The role of formal proof in modelling interactive behaviour
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.
KeywordsInteractive System Safety Property Usability Property Liveness Property Live Model
Unable to display preview. Download preview PDF.
- 2.D. Andrews and D. Ince. Practical formal methods with VDM. Series in software engineering. McGraw-Hill, 1991.Google Scholar
- 3.A. Blandford, R. Butterworth, and J. Good. Users as rational interacting agents: formalising assumptions about cognition and interaction. In Harrison and Torres , pages 43–60.Google Scholar
- 4.A. Blandford and R. Young. Specifying user knowledge for the design of interactive systems. Software Engineering Journal, pages 323–333, 1996.Google Scholar
- 6.R. Butterworth and D. J. Cooke. On biasing behaviour to the optimal. In Harrison and Torres , pages 291–306.Google Scholar
- 7.A. Dix. Formal Methods for Interactive Systems. Computers and People Series. Academic Press, 1991.Google Scholar
- 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.A. Hall. Seven myths of formal methods. IEEE Software, pages 11–19, September 1990.Google Scholar
- 16.B. Sufrin and J. He. Specification, analysis and refinement of interactive processes. In Harrison and Thimbleby , pages 153–199.Google Scholar
- 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