A formal technique for automated dialogue development

Abstract

A number of notations exist by which a designer can specify the behavior of a human-computer interface in relatively formal terms. In this paper we show how many of the dialogue specifications described using these notations are amenable to automated analysis to detect potential problems such as user actions that are never enabled or have effects that are hard to reverse. In many situations, a dialogue specification can be thought of as a finite state machine in which the transition between states is signalled as an event from the user or system. The trouble with this state transition model is that states quickly multiply presenting two problems to the analyst: (i) how to easily describe all of the possible dialogue states and state transitions; and (ii) how to analyze a very large STN. This paper reviews possible solutions to both of these problems. A tabular interface to Olsen's Propositional Production System is described and goes some way towards solving the descriptive problem. This representation is also useful for simulating requirements scenarios in a validation exercise. For the analytic problem, we make use of finite state model checking technology that allows for automated analysis of very large state machines. We demonstrate how eight categories of dialogue verification properties can be analyzed with this approach. Together, dialogue simulation and automated verification leads to a more complete analytic framework for dialogue development.