Formal modelling, in interactive system design, has received considerably less real use than might have been hoped. Formal methods can be expensive to use, with poor coverage of the design life cycle. In this paepr, 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 early 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 sepcification, 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.
展开▼
