The Z2SAL Home Page

Investigators

• John Derrick : refinement and model-checking
• Siobhán North : Z to SAL parser and translator
• Anthony Simons : Z mathematical toolkit in SAL

Summary

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 Z Notation, 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. The 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 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 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.