Abstract

This thesis addresses the applicability of automated deduction techniques in performing usability reasoning. Usability relates to how easily users will be able to operate a system. Hence, much of usability reasoning is done by placing users in front of the system andanalysing how they perform. (Formal) automated reasoning, on the other hand, is based on mathematics, and its aim is to enable precise reasoning about the world, from a model of that world. Automated reasoning is therefore without direct observation. The possibility of performing usability reasoning from early in the development process will contribute to a better understanding of the design, and reduce the problems found in later stages of development. The use of formality, will enable proof that certain desirable system properties are present. The use of automation will contribute to the quality of the analysis, and allow the analysis of more complex systems.

The thesis proposes an approach to verification which allows for a closer integration of verification into the interactive systems development life-cycle. This approach is based on a move towards a feature centric approach to verification. By promoting an integration of user oriented concerns into the verification process, the approach enables reasoning about human-factors related issues in a primarily software engineering oriented context.

A framework for usability related properties is also proposed. This framework is used to understand what is involved in reasoning about usability properties. A tool is developed which enables the verification of MAL-based interactor specifications in the SMV model checker. Examples are given of the application of both model checking and theorem proving to the analysis of usability properties, in the context of the proposed approach. These examples include analysis of how interface layout will support the users tasks, of whether interface design principles such as predictability are followed, and of mode complexity issues.