Building a refinement checker for Z

In previous work we have described how refinements can be checked using a temporal logic based model-checker, and how we have built a model-checker for Z by providing a translation of Z into the SAL input language. In this paper we draw these two strands of work together and discuss how we have impl...

Full description

Saved in:
Bibliographic Details
Published in:Electronic proceedings in theoretical computer science 2011-06, Vol.55 (Proc. Refine 2011), p.37-52
Main Authors: Derrick, John, North, Siobhán, Simons, Anthony J.H.
Format: Article
Language:English
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In previous work we have described how refinements can be checked using a temporal logic based model-checker, and how we have built a model-checker for Z by providing a translation of Z into the SAL input language. In this paper we draw these two strands of work together and discuss how we have implemented refinement checking in our Z2SAL toolset. The net effect of this work is that the SAL toolset can be used to check refinements between Z specifications supplied as input files written in the LaTeX mark-up. Two examples are used to illustrate the approach and compare it with a manual translation and refinement check.
ISSN:2075-2180
2075-2180
DOI:10.4204/EPTCS.55.3