English

Using Alloy to model-check visual design notations

Software Engineering 2008-02-18 v1 Symbolic Computation

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.

Cite

@article{arxiv.0802.2258,
  title  = {Using Alloy to model-check visual design notations},
  author = {Anthony J. H. Simons and Carlos Alberto Fernandez-y-Fernandez},
  journal= {arXiv preprint arXiv:0802.2258},
  year   = {2008}
}

Comments

8 pages

R2 v1 2026-06-21T10:13:02.614Z