Database of Research Tools Developed Using CADP

UMLAUT environment for UML

Organisation: IRISA/INRIA Rennes (FRANCE)

Functionality: Validation and test generation for UML specifications

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

Period: 1999/2000

Description: Since its standardization by the Object Management Group (OMG) in 1997, the Unified Modeling Language (UML) is becoming a de facto standard for describing telecommunication systems when following an object-oriented approach. But in spite of its richness, the semantics of this language is still informal and loosely defined. This makes harder the task of validating specifications of complex systems that involve concurrency and asynchronism. The use of formal methods, in particular verification techniques, is essential for ensuring the reliability of such systems. The author proposes to extend the UMLAUT environment, a toolset for the manipulation of UML models, with formal analysis techniques, in order to offer advanced software engineering capabilities to assist the design process of object-oriented systems.

The approach proposed consisted of identifying a precise operational semantics for a subset of UML, in order to enable the automatic construction of labelled transition systems (LTS) from UML specifications. This was done by first transforming an initial UML specification into an equivalent form that uses only relatively simple UML constructs (classes and basic operations), whose operational semantics is easier to define. Thus, the UML state machines have been transformed into UML classes and operations by appying the state design pattern, which roughly consists of representing states as instances of a particular class, and transitions as operations on objects of this class. The overall behaviour of the system is obtained by considering the interleaved execution of the control flows associated to the set of active objects.

This semantic definition allowed to construct a simulator for UML specifications within the UMLAUT environment. The simulator module allows to construct the LTS corresponding to an UML model in a demand-driven way. The simulator has been built using the OPEN/CAESAR environment of CADP for on-the-fly exploration of LTSs. This enabled a direct connection between UML and the CADP tools for on-the-fly verification, simulation, and testing (in particular, the test generator TGV). The approach is illustrated by specifying, verifying, and testing an Air Traffic Control system.

Conclusions: This work proved that formal verification techniques are applicable to UML specifications, by developing simulation tools based upon an operational interleaving semantics of UML. The connection of the UMLAUT environment to CADP enables the designer to validate UML models and automatically generate test suites using TGV. Further work concerns the integration of additional UML features (use cases, collaborations, etc.) in the formal framework, in order to facilitate the design of test purposes.

Publications: [Jezequel-Ho-LeGuennec-Pennaneach-99] J-M. Jézéquel, W.M. Ho, A. Le Guennec, and F. Pennaneac'h. "UMLAUT: An Extendible UML Transformation Framework". In R.J. Hall and E. Tyugu, editors, Proceedings of the 14th IEEE International Conference on Automated Software Engineering ASE'99, IEEE, 1999. Also available as INRIA Research Report RR-3775, October 1999.

Available on-line at:
or from our FTP site in PDF or PostScript

[LeGuennec-00] A. Le Guennec. "Méthodes formelles avec UML. Modélisation, validation et génération de tests". In M. Diaz and J-P. Courtiat and P. Senac, editors, Actes du Colloque Francophone pour l'Ingénierie des Protocoles CFIP'2000 (Toulouse, France), Hermès, octobre 2000.

Available on-line from our FTP site in PDF or PostScript

Alain Le Guennec
IRISA / Université de Rennes 1
Campus de Beaulieu
F-35042 Rennes Cedex
Tel: +33 (0)2 99 84 25 41
Fax: +33 (0)2 99 84 25 32

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

Last modified: Fri Feb 19 09:13:01 2016.

Back to the CADP research tools page