AUtoZ

AUtoZ is framework for UML diagram verification. Class and state diagrams are automatically transformed into Z, a formal language, which is then analysed and any inconsistencies are presented to the user.

UML suffers from a lack of formal semantics. This can cause ambiguities and inconsistencies to be introduced at the design stage of the software development lifecycle. AUtoZ aims to provide industrial-strength formal verification for UML class and state diagrams. AUtoZ is fully integrated into the eclipse development environment. Diagrams are drawn using eclipse's UML2 plugin, and verified using AUtoZ.

Diagram Verification

UML diagrams are drawn using eclipse's UML2 plugin The UML diagrams are verified by transforming them into a Z specification and then checking the specification using a Z type-checker. Any issues found with the Z specification are then presented to the user as error messages.

The Z specification that is generated is written in the ZOO style - a way of expressing object-oriented concepts using standard Z (standard Z isn't object-oriented). The transformation (or formalisation) is achieved by applying a set of FTL templates to the diagrams. The FTL templates capture patterns of ZOO specifications and are written in Z, with placeholders which diagrammatic elements populate upon application.

AUtoZ: A Framework

AUtoZ is a framework with a well-defined interface for connecting a Z tool. The design of AUtoZ considered a user who might wish to utilise AUtoZ's formalisation power with their own Z tool. The core of AUtoZ does all of the grunt work, allowing for implementations to focus on the Z tool interaction. During the initial development two flavours of AUtoZ were developed: AUtoCADiZ and AUtoZ/Eves. Due to the fact that both CADiZ and Z/Eves are no longer under active development, and because of the advances inside AUtoZ, these flavours of AUtoZ are no longer supported.

Current Version: AUtoCZT

The current implementation of the AUtoZ framework is AUtoCZT, which as the name suggests, uses CZT to parse and type-check the generated specification. Using CZT allows messages related to the Z specification to be mapped directly back to the UML diagrams (something lacking in previous flavours of AUtoZ). This is achieved by utilising CZT's XML mark-up for Z - ZML. This is explained in more detail in the related ABZ2010 paper.

Work-in-Progress

The following tasks are currently under development.

 

FTL Template Catalogue

An FTL Template Catalogue is a repository of knowledge and experience. It is envisaged to be an entity that evolves through use. We are currently developing a way to better manage templates. The aim is to allow users to write templates in pure FTL and automatically generate the execution language (EGL).

UML Operations

Work is in progress to determine an effective way of specifying how a class operation affects the system, without the user needing to write any Z (which is the current approach). One option is to use OCL for this; something which has been used in other tools of the same kind.

Publications

The following publications are related to AUtoZ.

 

J. R. Williams, F. A. C. Polack and R. F. Paige. Formal Analysis in Model Management: Exploiting the Power of CZT
ABZ 2010, LNCS 5977, p. 414, Springer-Verlag, February 2010
Paper | Presentation

J. R. Williams and F. Polack. Automated formalisation for verification of diagrammatic models
To appear in the proceedings of the 6th International Workshop on Formal Aspects of Component Software, Eindhoven, Netherlands, 2-3 November 2009
Paper | Presentation