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.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Derrick, John; Smith, Graeme: Temporal-logic property preservation under Z refinement (2012)
- Derrick, John; North, Siobhán; Simons, Anthony J.H.: Z2SAL: a translation-based model checker for Z (2011)
- Leuschel, Michael; Massart, Thierry: Efficient approximate verification of B and Z models via symmetry markers (2010)
- Roldán, Manuel; Durán, Francisco; Vallecillo, Antonio: Invariant-driven specifications in Maude (2009)
- Börger, Egon (ed.); Butler, Michael (ed.); Bowen, Jonathan P. (ed.); Boca, Paul (ed.): Abstract state machines, B and Z. First international conference, ABZ 2008, London, UK, September 16--18, 2008. Proceedings (2008)
- Derrick, John; North, Siobhán; Simons, Anthony J.H.: Z2SAL -- building a model checker for Z (2008)
Further publications can be found at: http://staffwww.dcs.shef.ac.uk/people/A.Simons/z2sal/publish.html