|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: http://www.inria.fr/rrrt/rr-3775.html or from the CADP Web 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 the CADP Web site in PDF
or
PostScript
|
| Contact: | 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 E-mail: Alain.Le_Guennec@irisa.fr |
| Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |
Back to the CADP research tools page