Support for Model Checking Z Specifications

One of the deficiencies in Z tools is that there is limited support for model checking Z specifications. It is found that building a model checker directly for a Z specification will take considerable effort and time due to an abstraction of the language. Translating a specification input on the Z language into a specification with language that an existing model checker tool accepts is an alternative method. Researchers at the University of Sheffield implemented a translation tool, which they called Z2SAL that took a Z specification and translated it into the input for Symbolic Analysis Laboratory (SAL), which is a framework for combining different tools for abstraction, program analysis, theorem proving and model checking. This paper discusses support for model checking Z specifications, in which the capability of Z2SAL is extended. This support includes a translation of a generic constant and a schema calculus. Instead of translating these aspects of the Z language into the SAL language as Z2SAL does, a Z specification containing these two notations will be pre-processed, in which a generic constant definition will be redefined to an equivalent axiomatic definition and a schema calculus definition will be expanded to a new schema definition. As a result, a redefined or expanded Z specification is generated, in which case a redefinition or an expansion can be performed, otherwise the Z specification input is returned. This paper discusses these supports.