Goal : Production of formal Z
from annotated UML diagrams
This site is under maintenance, please contact Yves.Ledru at imag.fr in case of
Latest news: the information that
appears on this page must be updated.
The latest developments about RoZ appear in our paper presented at
ZUM'06. A preliminary version can be found here:
"Using Jaza to animate RoZ
specifications of UML class diagrams"
Y. Ledru, ZUM'06, April 2006, postproceedings to appear by IEEE CS Press
If you are interested by the beta version of RoZ as presented in
the ZUM'06 paper, please contact directely
Yves.Ledru at imag.fr
- Consistency checking of UML specifications
Description of the tool
RoZ (named after the Rosetta stone) is a
of the CHAMPOLLION project whose goal is the integration of formal and
semi-formal methods for software development. The tool is integrated in
Rose environment. It allows the integration of data specification
in UML with formal annotations in
Z (or Object-Z)
language. Starting from an annotated specification, the tool
produces a formal specification by translating the UML
constructs and merging them with the annotations.
RoZ completes the UML
class diagram by automatically generating both UML
of elementary operations on the classes (attributes modifications,
and deleting objects of the class). The tool also allows to record a
for each operation and can generate corresponding proof obligations to
show that guards are consistent with the actual pre-conditions of these
operations. The Z-EVES prover
(from ORA) can be used to discharge these proof obligations.
In the future, we foresee the following evolutions for the tool:
with other model-based target languages (B, VDM,...), translation of
UML diagrams, verification of several consistency properties, the use
OCL as the annotation language.
RoZ is only a prototype version0.3. It is freely
distributed to academic institutions for non-profit use.
To obtain RoZ, please contact Yves.Ledru at imag.fr.
RoZ is based on the Rational Rose environment which can
try thanks to evaluation
Format of the tool
Rational Rose scripts to be run with a full or demo version of the
Rose tool (versions 4 and 98).
Unix Solaris 2.x, PC Windows NT/98/95
Z specifications in the LaTeX format
"Vers une intégration utile de notations semi-formelles et
: une expérience en UML et Z", S. Dupuy, Y. Ledru,
Chabre-Peccoud, Volume 6, numero 1, L'Objet, numero
méthodes formelles pour les objets, 2000
"An overview of RoZ - a tool for integrating UML and Z
S. Dupuy, Y. Ledru, M. Chabre-Peccoud, 12th Conference on Advanced
Systems Engineering (CAiSE'2000), 2000, to appear
"Vers une prise en compte des contraintes en UML grace
Z", S. Dupuy, INFORSID'2000, Lyon, France, Mai 2000
"Translating the OMT dynamic model into Object-Z" , S. Dupuy, Y.
M. Chabre-Peccoud, 11th International Conference of Z Users
LNCS 1493, Springer, 1998
"Identifying pre-conditions with the Z/EVES theorem prover" ,
Y. Ledru, 13th IEEE International Automated Software Engineering
Conf., IEEE CS Press, 1998
RoZ documentation (RTF
last update by Sophie
Dupuy, 22 february 2000