%0 Book Section
%A Siregar, Maria Ulfah
%B A Pre-processing Tool for Z2SAL to Broaden Support for Model Checking Z Specifications
%D 2018
%F digilib:39304
%I Springer International Publishing
%T A Pre-processing Tool for Z2SAL to Broaden  Support for Model Checking Z Specifications
%U https://digilib.uin-suka.ac.id/id/eprint/39304/
%V 561
%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, Z2SAL, that takes  a Z specification and translates it into the input for Symbolic Analysis  Laboratory (SAL), 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 original  Z specification is returned. Results show that the large number of our examples can be run successfully by our system. The redefined or expanded  Z specification can be translated later by Z2SAL and the generated SAL  file can be model checked or simulated by the SAL tool. Results also  show that Z2SAL can translate outputs of our system to some extent.  The majority of generated SAL files can be run by the SAL tool.