Database of Case Studies Achieved Using CADP

Object Modelling of Interactive Systems using UMLi.

Organisation: University of Manchester (UNITED KINGDOM)

Method: LOTOS

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

Domain: Human-Computer Interaction.

Period: 2002

Size: about 1600 lines of LOTOS

Description: UMLi (Unified Modelling Language for interactive applications) is an extension of UML dedicated to the design and implementation of user interfaces. Since the lack of a formal semantics for UML may lead to ambiguous interpretations of UML (and hence, UMLi) models, a formal semantics is needed for UMLi. This semantics is useful for implementing automated verification of models as well as interpretation of models to generate software code.

The approach chosen for providing a formal semantics for UMLi is to define a translation function from UMLi models to LOTOS specifications, which have a precisely defined semantics. Moreover, this also provides tool support for analysing UMLi models by using existing engineering environments for LOTOS, such as the CADP toolbox. The translation function from UMLi to LOTOS is specified by means of UMLi construct definitions (UCDs), which are definitions of UMLi constructs in terms of sets of (at least one) LOTOS construct.

The translation function is illustrated on a library system case-study. A LOTOS specification was generated automatically from the UMLi model of the library system. Using CADP, the labelled transition system corresponding to this LOTOS specification was generated, inspected by interactive simulation, and checked to be deadlock- and livelock-free.

Conclusions: The translation from UMLi to LOTOS provides the designers of interactive applications with a diagrammatic notation similar to UML and furthermore equipped with a formal semantics. This also provides automated analysis of interactive applications by using the verification capabilities of tool environments such as CADP.

Publications: [Pinheiro-02] Paulo Pinheiro da Silva. "Object Modelling of Interactive Systems: The UMLi Approach". PhD thesis, Department of Computer Science, University of Manchester, United Kingdom, 2002.
Available on-line at:
or from the CADP Web site PDF or PostScript
Paulo Pinheiro da Silva
Computer Science Department
Gates Building 2A, Room 242
Stanford University
Stanford, CA 94305-9020
Tel: (650) 723-1876
Fax: (650) 725-5850

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

Last modified: Thu Feb 11 12:22:02 2021.

Back to the CADP case studies page