IRISA/INRIA Rennes (FRANCE)
Validation and test generation for UML specifications
CADP (Construction and Analysis of Distributed Processes)
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.
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
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
Available on-line at: http://www.inria.fr/rrrt/rr-3775.html
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: http://cadp.inria.fr/software|