Overview

Although formal techniques are not widely used in the analysis of interactive systems there are reasons why an appropriate set of tools, suitably designed to be usable by system engineers, could be of value in the portfolio of techniques used to assess interactive systems. This chapter describes the role of formal techniques in modelling and analysing interactive systems, discusses unfulfilled opportunities and speculates about the removal of barriers to their use. It also presents the opportunities that a clear expression of the problem and systematic analysis techniques may afford.

Introduction

Formal approaches bring rigour and automation to usability engineering. Models capture key features of the interactive behaviour of the design and are then subjected to systematic analysis using verification techniques such as model checking (Clarke, Grumberg and Peled, 1999). The appropriate selection of models and verification techniques is critical to the value of the analysis. Otherwise models can bias the analysis and verification techniques can take the focus away from important safety or business-critical features of the designed interactive system.

Formal techniques have been used to analyse a variety of properties of interactive behaviours in a number of systems including menu structures in mobile phones, flight management systems and other control systems on aircraft, air traffic control systems, interaction techniques for virtual environments and many others. Two categories of (semi-)automated verification techniques can be identified.