A Translation from Alloy to B

Abstract

In this paper, we introduce a translation of the specification language Alloy to classical B. Our translation closely follows the Alloy grammar, each construct is translated into a semantically equivalent component of the B language. In addition to basic Alloy constructs, our approach supports integers and orderings. The translation is fully automated by the tool “Alloy2B”. We evaluate the usefulness by applying AtelierB and ProB to the translated models, and show benefits for proof and solving with integers and higher-order quantification.

Document

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.

Reference

% BibTex
@inproceedings{KringsSBFL18,
  author       = {Sebastian Krings and
                  Joshua Schmidt and
                  Carola Brings and
                  Marc Frappier and
                  Michael Leuschel},
  editor       = {Michael J. Butler and
                  Alexander Raschke and
                  Thai Son Hoang and
                  Klaus Reichl},
  title        = {A Translation from Alloy to {B}},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International
                  Conference, {ABZ} 2018, Southampton, UK, June 5-8, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10817},
  pages        = {71--86},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-91271-4\_6},
  doi          = {10.1007/978-3-319-91271-4\_6},
  timestamp    = {Wed, 25 Sep 2019 18:19:23 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/KringsSBFL18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}