Usability requirements as specification constraints: an example of WYSIWYG

The paper describes the application of formal modelling techniques within interface design to a `what you see is what you get´ style word processor to illustrate the analysis of the usability properties of interactive systems. A formal framework as an abstract model interaction is employed, termed the template model, which explicitly identifies system abstractions (known as templates) that have a defined relationship to the intended task and users´ capabilities. In the investigation, a subset of a conventional word processor is formally specified. The specification is then analysed in terms of the template model by identifying abstractions upon which common word-processing tasks depend. The outcome of the analysis illustrates the potential benefit of the template model in explaining implicit assumptions about the usability properties of the artefact