A Pre-processing Tool for Z2SAL to Broaden Support for Model Checking Z Specifications

Siregar, Maria Ulfah A Pre-processing Tool for Z2SAL to Broaden Support for Model Checking Z Specifications. In: A Pre-processing Tool for Z2SAL to Broaden Support for Model Checking Z Specifications. Springer International Publishing.

Preview

Text (A Pre-processing Tool for Z2SAL to Broaden Support for Model Checking Z Specifications) PreprocessingToolforZ2SAL.pdf - Published Version Download (413kB) | Preview

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, 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.

Share this knowledge with your friends :

Actions (login required)

View Item