(pronounce it "Rosette") - Production of formal Z specifications from annotated UML diagrams
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.
"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"
13th IEEE International Automated Software Engineering Conf., IEEE CS Press, 1998
RoZ is freely distributed to academic institutions for non-profit use.
RoZ can be downloaded at the following URL:
Contact persons : S. Dupuy (Sophie.Dupuy@imag.fr) and Y. Ledru (Yves.Ledru@imag.fr)
Rational Rose scripts to be run with a full or demo version of the Rational Rose tool (versions 4 and 98)
Unix Solaris 2.x, PC Windows NT/98/95
Z specifications in the LaTeX format