Crucible Tools for Test Generation and Animation of Alloy Models

Abstract

Crucible is a suite of tools supporting the use of Alloy as a functional specification language for high-integrity software systems. It incorporates a test generator, animator and range of supporting tools. Test generation is achieved by producing test conditions from the input Alloy model, and then using the Alloy Analyzer to produce solutions. The solutions can optionally be converted into executable tests targeting a range of implementation languages. The animator allows scenarios to be defined by users and run to help stakeholders validate the Alloy model. In this paper, we provide an overview of the Crucible tools.

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{WilsonM23,
  author       = {Thomas Wilson and
                  Stuart Matthews},
  editor       = {Uwe Gl{\"{a}}sser and
                  Jos{\'{e}} Creissac Campos and
                  Dominique M{\'{e}}ry and
                  Philippe A. Palanque},
  title        = {Crucible Tools for Test Generation and Animation of Alloy Models},
  booktitle    = {Rigorous State-Based Methods - 9th International Conference, {ABZ}
                  2023, Nancy, France, May 30 - June 2, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14010},
  pages        = {116--123},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-33163-3\_9},
  doi          = {10.1007/978-3-031-33163-3\_9},
  timestamp    = {Fri, 02 Jun 2023 21:23:53 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/WilsonM23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}