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.
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.
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).
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.
The following publications are related to AUtoZ.
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