UML + Z: Augmenting UML with Z.

*
UML + Z
*
is a framework for building, analysing and refining
models of software systems based on the UML and the formal specification
language Z. It is, in fact, an instance of an approach to build rigorous
engineering frameworks for model-driven development based on templates,
which we call is targeted at developers
who have minimal knowledge of Z, but are familiar with UMLbased
modelling.
*
UML + Z
*
models comprise class, state and object UML
diagrams, which are represented in a common Z model (the semantic
domain); the Z model gives the precise meaning of the diagrams. The
framework tries to minimise exposure to the Z model, with UML diagrams
acting like a graphical interface for the formality (Z) that lies
underneath; but this is not always possible and one Z expert is required
in the development to describe system properties that are not
expressible diagrammatically (mainly operations and constraints).

A crucial component of
*
UML + Z
*
is a catalogue of
*
templates
*
and
*
meta-theorems
*
. Templates are generic representations of
sentences of some formal language, which, when instantiated, yield
actual language sentences. To express templates, we have developed the
formal template language (FTL), which enables an approach to proof with
template representations of Z (
*
meta-proof
*
). This allows the
representation of structural Z patterns as templates (e.g. the structure
of a Z operation), but also reasoning with these template representation
to establish meta-theorems (e.g. calculate a precondition). Every
sentence of the Z model in
*
UML+Z
*
is generated by instantiating
one of the templates, and meta-theorems can be used to simplify, and in
some cases fully discharge, proofs associated with the Z model.

The modelling and analysis process with
*
UML + Z
*
begins with
the drawing of UML class and state diagrams. These diagrams are then
used to instantiate templates from the catalogue to generate the Z
model. The developer then adds operations and system constraints that
are not expressed diagrammatically to the Z model. The Z specification
is then checked for consistency using the meta-theorems of the
*
UML+Z
*
catalogue and a Z theorem prover. Finally, there is a process of model
analysis, where the developer draws snapshots to validate the model;
these snapshots are represented in Z and the analysis is assisted by the
Z/Eves theorem prover. Usually, the analysis phase of the process
results in changes to the diagrams or the portion of the Z model not
expressed diagrammatically.

**
Full chapter
**
:
PDF
137K

@incollection(SS-UMLZ-06, author = "Nuno Am\'{a}lio and Fiona Polack and Susan Stepney", title = "UML + Z: UML augmented with Z", crossref = "SSM-06" ) @book(SSM-06, editor = "Marc Frappier and Henri Habrias", title = "Software Specification Methods : an Overview Using a Case Study, new edn", booktitle = "Software Specification Methods : an Overview Using a Case Study, new edn", publisher = "Hermes Science Publishing", year = 2006 )