Formal Methods

Download early version of full paper (PDF, 329K).

Full reference:

A. J. Dix (1995). Formal Methods.
In Perspectives on HCI: Diverse Approaches, Eds. A. Monk and N. Gilbert. London, Academic Press. pp. 9-43.
http://www.hcibook.com/alan/papers/formal-chapter-95/

for related work see http://www.hcibook.com/alan/topics/formal/

Abstract

This chapter appeared in Andrew Monk and Nigel Gilbert's collection "Perspectives on HCI". This book contains chapters from experts in a variety of disciplines contributing to HCI. This chapter is about the use of formal methods in HCI.

The chapter is organised around three major uses of formalism within HCI:

• Specification of individual interactive systemsnotations to describe the intended interactive behaviour of specific systems
  
• Generic models of interactive systemsmodels that allow reasoning about broad properties such as the meaning of undo
  
• Dialogue specification and analysisnotations, often diagrammatic, for describing the navigational or dialogue structure of applications
  

The chapter is written assuming a broad audience and the small amount of set and function notation used within it is explained within the chapter.

Keywords formal methods, HCI, undo, formal specification, dialogue notation, dialogue analysis, PIE model

2.1 Introduction

For many years I have worked on the interplay between formal methods and human-computer interaction. This area of research originated with (present and past) workers from York, but over the last few years there have been several international workshops on the subject and there are now several books on aspects of this area. For further reading in the area the interested reader can consult the chapters on Dialogue and Formal Methods in (Dix et al., 1993), my previous monograph (Dix, 1991) and the collection (Harrison and Thimbleby, 1990).

2.1.1 Why use formal methods?

Formal notations and mathematics are used in several areas of human-computer interaction, including cognitive modelling and task analysis. However, this chapter will focus on those more connected with the engineering and analysis of interactive systems. These notations all try to abstract away from the way the system is programmed, but still be precise about some aspect of its behaviour. Of course, an informal description does the same, but with a formal description you can (in theory) say precisely whether or not a real system satisfies the description. Because of this, one can perform precise analyses on the description itself, knowing that any conclusions one comes to will be true of the real system.

One value of this precision is that it exposes design decisions which otherwise might not be noticed until the system is being implemented. It is clear in many systems that obscure interface behaviour could not have been designed that way, but has occurred as the result of some programming decision. The specification of an interactive system should not determine the algorithms and data structures used to build the system – that is the proper domain of the programmer. But, it should describe precisely the behaviour of the system – the programmer may not be qualified to make such decisions and the level of commitment at the time that the issue is uncovered may mean that the design choice has been determined by foregoing implementation choices.

2.1.2 Uses of formal methods

We will consider three major strands of formal methods, each of which fulfils a different purpose:

Specification of individual interactive systems

This usually concentrates on a specific system and the complete specification of all aspects of its behaviour. Its purpose is to clarify design decisions, to expose inconsistency and to act as a ‘contract’ with the implementor. User interface software can be extremely complex and so being able to deal with it at a more abstract level is even more important than for general software.

Generic models of interactive systems

The second strand models classes of system, for example, one might have a general model of window managers as opposed to a specific model of the Macintosh window manager. Their purpose is to give new insight into general problems as the properties of the problem domain are analysed. For example, we will see later how general questions about the meaning of the undo command can be addressed without recourse to a specific system. In addition, they can be used as part of a formal development process to constrain the design of specific systems. That is, results of the analysis of generic models can be applied to formal specifications of specific systems.

Dialogue specification and analysis

Finally, dialogue notations are again used to describe specific systems, but at a different level of detail than a full formal specification. They concern the steps of the user interaction but typically do not fully specify the meaning attached to the user’s actions. For example, the dialogue specification of a graphics editor may say that the user must always enter two positions (by mouse clicks) after selecting the ‘draw line’ icon. However, it will not say that a line appears in the screen, except perhaps by way of informal annotation. Dialogue notations are used for various reasons, but this chapter will emphasise the way the formal element in the dialogue can be analysed in order to expose potential user interface problems.

2.1.3 What is formal anyway?

Of these three strands, dialogue specification is perhaps least mathematical, but most easily used by the non-formalist. Indeed, although formal methods can be extremely powerful they do require a high-level of expertise. Most computing courses now include some element of formal methods and so the level of formal expertise will increase in coming years. However, it is unlikely that there will ever be a large community of people expert in both human factors and formal methods.

This suggests that formal methods need to packaged so that non-experts can get some of the benefits without negotiating the steep learning curve. One way this can be achieved is through ‘engineering level’ notations which have formal underpinnings, but where simplified analysis and heuristics can be applied. This is as in other disciplines where the practising engineer does not use the theoretical methods and analyses directly, but instead more pragmatic and approximate versions of them. In the user interface domain, dialogue notations are one example of an engineering level notation and are amenable to both simple hand analysis and automated tool support. The fact that many dialogue notations have a graphical form also makes them more palatable! Another example of an engineering level notation is status/event analysis which uses simple timeline diagrams together with design heuristics based on a combination of formal analysis and naïve psychology (Dix, 1991, Ch. 10, Dix, 1992, Dix et al., 1993, Ch. 9).

Sometimes the benefits of formal analysis can be presented informally. For example, a purist might argue that an undo button should always undo the effects of the last command - even if the last command was itself undo. However, we shall see later that this is in fact impossible, thus removing the cause of long arguments and allowing more constructive debate over the purpose of undo. Not only can we state the result 'it is impossible' in this case the formal proof can be rendered in a reasonably informal, but convincing manner - which is as well as no-one ever believes the result!

Of course, we can all recognise a bit of formal notation - simply watch out for the ! However, you will find that the dialogue notations are mostly diagrammatic. Can a graphical notation be formal? In fact, a diagram can be formal, informal or somewhere in between, depending on the meaning which s attached to the elements of the diagram. This is obvious when we think of an engineering diagram. When it says that the diameter of a rod is 13.7 mm it means precisely that! The dialogue notations discussed in this chapter will be semi-formal in that they have textual annotations on the diagrams which require informal interpretation. However, the structure of the diagrams will be perfectly formal and capable of formal analysis. The counterside of this also needs to be considered. Just because a paper is filled with Greek and upside down letters doesn't mean it is formal!

Any formal notation abstracts in some way. In being very precise about some things it completely ignores others. The important thing is to be aware of what is being abstracted and whether the abstraction is appropriate for the purpose for which it is required.

In the next chapter a computer game is specified in Z, a particular formal notation. It is thus an example of the first strand of formal methods. In the rest of this chapter we will look at the other two strands in more detail. We will begin with a short introduction to the language and concepts used in formal methods.