Models of interactive systems: a case study on programmable user modelling

摘要

Models of interactive systems can be used to answer focused questions about those systems. Making the appropriate choice of modelling technique depends on what questions are being asked. We present two styles of interactive system model and associated verification method. We show how they contrast in terms of tractability, inspectability of assumptions, level of abstraction and reusability of model fragments. These trade-offs are discussed. We discuss how they can be used as part of an integrated formal approach to the analysis of interactive systems where the different formal techniques focus on specific problems raised by empirical investigations. Explanations resulting from the formal analyses can be validated with respect to the empirical data. The first modelling style, which we term 'operational', is derived directly from principles of rationality that constrain which user behaviours are modelled. Modelling involves laying out user knowledge of the system and task, and their goals, then applying the principles to reason about the space of rational behaviours. This style supports reasoning about user knowledge and the consequences of particular knowledge in terms of likely behaviours. It is well suited to reasoning about interactions where user knowledge is a key to successful interaction. Such models can readily be implemented as computer programs; one such implementation is presented here. Models of the second style, 'abstract', are derived from the operational models and thus retain important aspects of rationality. As a result of the simplification, mathematical proof about selected properties of the interactive system, such as safety properties, can be tractably applied to these models. This style is well suited to cases where the user adopts particular strategies that can be represented succinctly within the model. We demonstrate the application of the two styles for understanding a reported phenomenon, using a case study on electronic diaries. (C) 2003 Elsevier Ltd. All rights reserved. [References: 67]