RoZ (pronounce it "Rosette")

Goal : Production of formal Z specifications from annotated UML diagrams

This site is under maintenance, please contact Yves.Ledru at in case of problems.

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

Main Functionalities

Derived Functionalities

Description of the tool

RoZ (named after the Rosetta stone) is a product of the CHAMPOLLION project whose goal is the integration of formal and semi-formal methods for software development. The tool is integrated in the Rational Rose environment. It allows the integration of data specification expressed in UML with formal annotations in the Z (or Object-Z) language. Starting from an annotated specification, the tool automatically 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 and Z specifications of elementary operations on the classes (attributes modifications, adding and deleting objects of the class). The tool also allows to record a guard 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: compatibility with other model-based target languages (B, VDM,...), translation of other UML diagrams, verification of several consistency properties, the use of 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
RoZ  is based on the Rational Rose environment which can freely  try thanks to evaluation copies.

Format of the tool

Rational Rose scripts to be run with a full or demo version of the Rational Rose tool (versions 4 and 98).

Supported platforms

Unix Solaris 2.x, PC Windows NT/98/95

Input format


Output format

Z specifications in the LaTeX format

Related papers

"Vers une intégration utile de notations semi-formelles et formelles : une expérience en UML et Z",   S. Dupuy, Y. Ledru, M. Chabre-Peccoud, Volume 6, numero 1, L'Objet,  numero spécial méthodes formelles pour les objets, 2000

"An overview of RoZ - a tool for integrating UML and Z specifications",  S. Dupuy, Y. Ledru, M. Chabre-Peccoud, 12th Conference on Advanced information 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. Ledru, M. Chabre-Peccoud,  11th International Conference of Z Users (ZUM'98), 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 version, postscript version)

 last update by  Sophie Dupuy, 22 february 2000