Features and Benefits .
Future Research
Availability .
Related Works .
Links
Roze (Rose with Z) is the resulting add-in from the experience in the formalization of UML class diagrams using formal methods. It is just a small part of ForMULa project, whose main goal is to provide a formal background to UML-RT, a not so formal notation to express real-time systems.
Roze provides three options to the user, which are shown below. In the first one, we annotate the UML diagram with Object-Z LATEX macros. In the second and third ones, just the classes (and their respective association, if applicable) are annotated with Z LATEX macros.
Generate Object-Z. This generates a full Object-Z specification from an annotated UML class diagram. In this approach, we can syntax- and type-check the specification using the Wizard, which allows us to identify main errors on the UML model.
Z Property Checker. In this approach, Roze generates a full Z specification from an annotated UML class, verifying properties using the Z/EVES prover.
Z Refinement. Here, Roze generates a full Z specification from two annotated UML classes and their respective <
Roze if fully integrated with Rational Rose, which allows us to use it without leaving the modelling environment. Through it, we can automatically generate Object-Z and Z specifications from annotated UML class diagrams. This allows the verification of the diagram using formal tools, as Wizard or Z/EVES. So, the great benefits that we can obtain is the use of a formal process hidden in the UML notation, guaranteeing the overall quality of critical and complex systems.
As future research, we intend to extend our graphical notation to UML-RT, a UML extension able to model real-time systems, as well as our formal language to OhCircus, in order to capture static and dynamic aspects of systems simultaneously, and providing a uniform way of deriving program code from specifications.
The Roze tool is a free tool available for download and only works in Windows, because of ActiveX technology. It uses the Rational Rose, which can be freely tried, and generates Object-Z or Z specifications in LATEX notation.