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.

[img]
Preview
Text
thesis_acp12mus_rev.pdf
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (1967Kb) | Preview

Abstract

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)
Depositing User: Mrs Maria Ulfah Siregar
Date Deposited: 10 Jul 2017 08:24
Last Modified: 10 Jul 2017 08:24
URI: http://etheses.whiterose.ac.uk/id/eprint/17776

Actions (repository staff only: login required)