RoZ : a tool to integrate graphical and formal notations

RoZ (pronounce it "Rosette") is named after the Rosetta stone. It links graphical and formal notations by translating a class diagram annotated by formal assertions, written in the Z specification language, into a Z specification. There are two major versions of RoZ:

• RoZv1.0 is the initial version of RoZ, which addressed class diagrams produced with Rational Rose. This version is now deprecated.
• RoZv2.0 is the current version. It generates Z specification from eclipse/papyrus UML class diagrams.

RoZ is used in combination with JazaGUI, a user interface for the jaza Z animator.