University of Manchester (UNITED KINGDOM)
CADP (Construction and Analysis of Distributed Processes)
about 1600 lines of LOTOS
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.
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.
[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
Paulo Pinheiro da Silva
Computer Science Department
Gates Building 2A, Room 242
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: http://cadp.inria.fr/case-studies|