|

Z to SAL

Research by

Summary

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.

Related projects