eprintid: 39305
rev_number: 8
eprint_status: archive
userid: 12308
dir: disk0/00/03/93/05
datestamp: 2020-05-21 00:20:27
lastmod: 2020-05-21 00:20:27
status_changed: 2020-05-21 00:20:27
type: conference_item
metadata_visibility: show
contact_email: maria.siregar@uin-suka.ac.id
creators_name: Siregar, Maria Ulfah
title: Support for Model Checking Z Specifications
ispublished: pub
subjects: TB
divisions: artkl
full_text_status: public
pres_type: paper
abstract: 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.
event_title: FMi 2016 in IRI 2016
event_type: conference
refereed: TRUE
citation:   Siregar, Maria Ulfah   Support for Model Checking Z Specifications.  In: FMi 2016 in IRI 2016.     
document_url: https://digilib.uin-suka.ac.id/id/eprint/39305/1/SupportforModelCheckingZSpec.pdf