Pragmatic Formal Design: A Case Study in Integrating Formal Methods into the HCI Development Cycle

Formal modelling, in interactive system design, has received considerably less real use than might have been hoped. Heavy weight formal methods can be expensive to use, with poor coverage of the design life cycle. In this paper, we suggest a pragmatic approach to formal design. We rely on a range of models that can help at different stages of development. We use as a case study, the design of a multi-user, design rationale editor. In the initial stages of our design, we use a range of semi-formal notations, to perform a task analysis. We then develop a prototype in Clock, a high level functional language. From this, we derive a LOTOS specification, which we use to verify that our system satisfies important design requirements. The task analysis helps here, in highlighting these requirements. Throughout we rely on tool support to simplify the process, and so make it cost effective.

• Type: Conference
• Year: 1998
• Where: DSVIS
• Authors: Meurig Sage, Chris Johnson
• Keywords: Computer Human Interaction, Design Life Cycle, DSVIS 1998, Task Analysis, Weight Formal Methods