Overview:

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.

@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
)