Complex computer systems are difficult to implement correctly. To aid
the process formal methods use mathematics in the specification of a
systems requirements and its refinement into more detailed designs and
program code. In this project we are concerned with providing tool
support for the formal specification
language Z.
Z has been very successful and a number of groups are currently
developing usable tool support for it. The
CZT (Community Z Tools)
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
this 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.
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
and CTL.
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 command line interface, where input format is LaTeX markup as
given in the Z standard, and output is a SAL file upon which the SAL
tools can be applied.
We currently have a beta version of the tool available.