swMATH ID: 7087
Software Authors: J Derrick, S North, A J H Simons
Description: Z2sal: a translation-based model checker for z. 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.
Homepage: http://staffwww.dcs.shef.ac.uk/people/A.Simons/z2sal/
Keywords: model checker; z
Related Software: SPIN; Z; Z/EVES; CZT; jSpin; PROMELA; SymmSpin; Spin-to-Grape; Atelier B; B4Free; ProB; Rodin; Uppaal; TopSpin; nauty; Jaza; KeY; Maude; OBJ3; Stratego
Cited in: 5 Publications
Further Publications: http://staffwww.dcs.shef.ac.uk/people/A.Simons/z2sal/publish.html

Citations by Year