%0 Conference Paper
%A Siregar, Maria Ulfah
%B FMi 2016 in IRI 2016
%F digilib:39305
%T Support for Model Checking Z Specifications
%U https://digilib.uin-suka.ac.id/id/eprint/39305/
%X One of the deficiencies of Z tools is that there is limited  support for model checking Z specifications. Building a model checker  directly for a Z specification will take considerable amount of effort and  time due to the abstraction of the language. Translating a Z specification input into a specification in a 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 takes a Z specification and translates 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  definition. 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  is redefined to an equivalent axiomatic definition and a schema calculus  definition is expanded to a new schema definition. As a result of a successful redefinition or expansion, a redefined or expanded Z specification  is generated, otherwise the Z specification input is returned.