White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Support for Model Checking Z Specifications

Siregar, Maria Ulfah (2016) Support for Model Checking Z Specifications. PhD thesis, University of Sheffield.

Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (1967Kb) | Preview


One of deficiencies in the Z tools is that there is limited support for model checking Z specifications. To build a model checker directly for a Z specification would take considerable effort and time due to the abstraction of the language. Translating inputs of a Z specification into a language that an existing model checker tool accepts is an alternative method. Researchers at the University of Sheffield implemented a translation tool which took a Z specification and translated it into the input for the Symbolic Analysis Laboratory (SAL) tool, a framework for combining different tools for abstraction, program analysis, theorem proving and model checking, which they called Z2SAL. In this paper, support for model checking Z specifications is discussed, in which the ability of the existing Z2SAL is extended. This support includes a translation for generic constant and 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 its equivalent axiomatic definition, and schema calculus will be expanded to a new schema definition. This paper discusses the implementation of these types of support, and illustration of some working examples. The discussion also includes other several issues related to a new approach in translating Z functions and constants in SAL language, which originates from the type incompatibility obtained during execution by the SAL tool, an approach to a SAL translation of embedded theorems on Z specifications, and a manual experiment on applying an abstraction on Z specifications. Results have been gathered during our experiments with the implemented support. Several of these results could be translated by Z2SAL and be executed by the SAL tool.

Item Type: Thesis (PhD)
Keywords: Z, Generic Constant, Schema Calculus, Z2SAL, SAL, Model Checking
Academic Units: The University of Sheffield > Faculty of Engineering (Sheffield) > Computer Science (Sheffield)
The University of Sheffield > Faculty of Science (Sheffield) > Computer Science (Sheffield)

The University of Sheffield > Faculty of Engineering (Sheffield)
Identification Number/EthosID: uk.bl.ethos.718818
Depositing User: Mrs Maria Ulfah Siregar
Date Deposited: 10 Jul 2017 08:24
Last Modified: 12 Oct 2018 09:41
URI: http://etheses.whiterose.ac.uk/id/eprint/17776

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)