A Design Life-Cycle for the Formal Design of User Interfaces

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. We propose a software design life cycle integrating formal task and system modelling. 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 on the life cycle. 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.