The Z2SAL Home Page
Complex computer systems are difficult to implement correctly. To aid
in the process, formal methods use mathematics in the specification of a
system's requirements and its refinement into more detailed designs and
program code. In this project we are concerned with providing tool
support for the
a widely-used formal specification language.
Z has been very successful in academia and industry; and a number of
groups are currently developing usable tool support for it. The
Community Z Tools (CZT)
project is building a set of tools for editing, typechecking and
animating formal specifications written in the Z, with some support for
Z extensions such as Object-Z, Circus, and TCOZ. These tools are all
built using the CZT Java framework for Z tools.
In the Z2SAL project we are implementing a model checker for Z
by providing a translation between Z and the SAL toolkit. The work is
part of a collaboration with the University of Queensland, Australia.
Symbolic Analysis Laboratory (SAL) is a tool-suite
for the analysis and verification of systems specified as
state-transition systems. It allows different verification tools to be
combined, all working on an input language designed as a format into
which programming and specification languages can be translated. The
input language provides a range of features to support this aim, such as
guarded commands, modules, definitions etc., and can, in fact, be used
as a specification language in its own right. The tool-suite currently
comprises a simulator and four model checkers including those for LTL
The translation scheme preserves the Z-style of specification
including predicates where primed and unprimed variables are mixed, and
the approach of the Z mathematical toolkit to the modelling of
relations, functions etc., as sets of tuples. Our current implementation
uses a simple Java interface, where the input format is LaTeX markup as
given in various Z styles, and output is a SAL file upon which the SAL
tools can be applied.
We currently have a beta version of the tool available —
see the download page.