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: http://www.ksl.stanford.edu/people/pp/papers/PinheirodaSilva_PhD_2002.pdf or from the CADP Web site PDF or PostScript
Contact:	Paulo Pinheiro da Silva Computer Science Department Gates Building 2A, Room 242 Stanford University Stanford, CA 94305-9020 USA Tel: (650) 723-1876 Fax: (650) 725-5850 E-mail: pp@ksl.stanford.edu
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page