The information listed on this page refers to the state of the tool in '99. For more recent information, please use the following link:

http://www-lsr.imag.fr/Les.Groupes/pfl/RoZ

---

RoZ - LSR

Name of the tool : RoZ

(pronounce it "Rosette") - Production of formal Z specifications from annotated UML diagrams

Main Functionalities

• Automatic translation of annotated UML class diagrams into Z specifications
• Synthesis of both UML and Z specifications of elementary operations associated to a class diagram
• Generation of proof obligations related to operation guards
• Integration in the Rational Rose(TM) environment

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 (TM) 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.

Related papers

"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

Availability

RoZ is freely distributed to academic institutions for non-profit use.

address

RoZ can be downloaded at the following URL:

http://www-lsr.imag.fr/Les.Groupes/pfl/RoZ/

Contact persons : S. Dupuy (Sophie.Dupuy@imag.fr) and Y. Ledru (Yves.Ledru@imag.fr)

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