Using Alloy to model-check visual design notations
Anthony J. H. Simons, Carlos Alberto Fernandez-y-Fernandez
TL;DR
This paper demonstrates how Alloy can be used to model-check the syntax of UML diagrams in the Discovery Method, ensuring their validity through formal specification and verification.
Contribution
It introduces a unified Alloy specification for UML diagrams in the Discovery Method and shows how to verify diagram validity automatically.
Findings
Alloy effectively models UML diagram syntax.
Automated validation improves diagram correctness.
Unified specification covers multiple UML diagram types.
Abstract
This paper explores the process of validation for the abstract syntax of a graphical notation. We define an unified specification for five of the UML diagrams used by the Discovery Method and, in this document, we illustrate how diagrams can be represented in Alloy and checked against our specification in order to know if these are valid under the Discovery notation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.