RoZ (pronounce
it "Rosette")
Goal : Production of formal Z
specifications
from annotated UML diagrams
This site is under maintenance, please contact Yves.Ledru at imag.fr 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 imag.fr
Main Functionalities
Derived Functionalities
- Consistency checking of UML specifications
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.
Availability
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
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
N/A
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