Few tools are available to help with the difficult task of validating that a Z specification captures its intended meaning. One tool that has been proven to be useful for validating specifications is the Alloy Analyzer, an interactive tool for checking and visualising Alloy models. However, Z specifications need to be translated to Alloy notation to make use of the Alloy Analyzer. These translations have been performed manually so far, which is a cumbersome and error-prone activity. The aim of this paper is to explore to what extent this process can be automated. The paper identifies a subset of Z that can be straightforwardly translated to Alloy, and the translation for this subset is formalised. More complex constructs, like schemas, are harder to translate. The paper gives a brief overview of the problems, and discusses alternative translation approaches.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{MalikGL10,
author = {Petra Malik and
Lindsay Groves and
Clare Lenihan},
editor = {Marc Frappier and
Uwe Gl{\"{a}}sser and
Sarfraz Khurshid and
R{\'{e}}gine Laleau and
Steve Reeves},
title = {Translating {Z} to Alloy},
booktitle = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
{ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5977},
pages = {377--390},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-11811-1\_28},
doi = {10.1007/978-3-642-11811-1\_28},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/MalikGL10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}