Improving the Visualization of Alloy Instances

Rui Couto
(HASLab/INESC TEC & University of Minho)
José C. Campos
(HASLab/INESC TEC & University of Minho)
Nuno Macedo
(HASLab/INESC TEC & University of Minho)
Alcino Cunha
(HASLab/INESC TEC & University of Minho)

Alloy is a lightweight formal specification language, supported by an IDE, which has proven well-suited for reasoning about software design in early development stages. The IDE provides a visualizer that produces graphical representations of analysis results, which is essential for the proper validation of the model. Alloy is a rich language but inherently static, so behavior needs to be explicitly encoded and reasoned about. Even though this is a common scenario, the visualizer presents limitations when dealing with such models. The main contribution of this paper is a principled approach to generate instance visualizations, which improves the current Alloy Visualizer, focusing on the representation of behavior.

In Paolo Masci, Rosemary Monahan and Virgile Prevosto: Proceedings 4th Workshop on Formal Integrated Development Environment (F-IDE 2018), Oxford, England, 14 July 2018, Electronic Proceedings in Theoretical Computer Science 284, pp. 37–52.
Published: 27th November 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: