Synergistic modelling of tasks, users and systems using formal specification techniques

This paper aims at clarifying the articulation between the task models and system models encountered in CHI design practices. We demonstrate how the use of a formal task model may enhance the design of interactive systems, by providing quantitative results on which designers may base their decisions. We also demonstrate that it is possible to describe both task and system models within the same formal framework. This enables us firstly to formally prove that task and system models comply with each other, and secondly to perform quantitative analysis on the combination of task and system models. The approach is illustrated by a toy example which, despite its small size, allows us to develop both task and device models, and to perform several iterations of the design process. The device and tasks are modelled using the Interactive Cooperative Objects (ICO) formalism, which is based on Petri nets and on the object-oriented approach. The formality of Petri nets allows for axiomatic validation of isolated and interacting subsystems.