Database of Case Studies Achieved Using CADP

Multi-user Design Rationale Editor.

Organisation: Glasgow Interactive Systems Group, Department of Computing Science, University of Glasgow (SCOTLAND)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Human-Computer Interaction.

Period: 1998.

Size: n/a

Description: This work proposes a pragmatic approach to formal design of interacting systems, that aims to: re-use existing techniques, make good use of tool support to assist design stages, and provide good coverage for all stages of the development. This approach is illustrated by means of a case-study concerning the design of a multi-user design rationale editor, for which significant design decisions are needed and where concurrency is required.

Design rationale is supported by QOC (Questions, Options, and Criteria), a graphical semi-formal notation that highlights the key questions in a design and links them with possible options and criteria supporting those options. The design rationale editor allows several users to build a QOC rationale by creating nodes (Questions, Options or Criteria) and connecting them together. Users can modify nodes in mutual exclusion, note their actions in a shared log, and hide or view certain nodes to make browsing easier.

The system is designed using an iterative development method with several stages. The first stage is requirements elicitation, which relies here on previous observational studies on design rationale. Next, the high-level task analysis stage is performed using the ConcurTaskTree notation, which combines a graphical tree-like representation with LOTOS composition operators. The next two stages, detailed interaction and prototyping, are carried out using UAN (User Action Notation) and the Clock language, respectively.

The final stage in the development, namely establishing task conformance properties, is performed by means of formal verification. To achieve this, the Clock implementation of the system is translated into an interactor network described in LOTOS and the EVALUATOR tool of CADP is used to check the locking properties previously established during the task analysis.

Conclusion: The development of interactive systems requires a variety of modelling approaches. In the early stages of development, lightweight models that can be used to give multiple views on a system are particularly useful. In addition, prototyping languages like Clock can help the development process. The ability to derive automatically LOTOS specifications from Clock prototypes, and then perform analysis of these specifications using appropriate verification toolsets such as CADP, makes the use of formal specifications more cost effective.

Publications: [Sage-Johnson-98] Meurig Sage and Chris Johnson. "Pragmatic Formal Design: A Case Study in Integrating Formal Methods into the HCI Development Cycle". In: Proceedings of the 5th International Eurographics Workshop on Design, Specification, and Verification of Interactive Systems DSV-IS '98 (Abingdon, UK), June 1998.
Available on-line at:
or also from the CADP Web site in PDF or PostScript
Chris Johnson
Department of Computing Science
University of Glasgow
G12 8QQ
Tel: +44 141 330 6053
Fax: +44 141 330 4913

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Wed Apr 20 15:57:10 2022.

Back to the CADP case studies page