Title :
Using Alloy to model-check visual design notations
Author :
Simons, Anthony J H ; Fernández, Carlos Alberto Fernández y
Author_Institution :
Dept. of Comput. Sci., Sheffield Univ., UK
Abstract :
This paper explores the process of validation for the abstract syntax of a graphical notation. We define a 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.
Keywords :
Unified Modeling Language; formal specification; program verification; Alloy model checker; UML diagram; Unified Modeling Language; abstract syntax; discovery method; formal specification; graphical notation; visual design notation; visual model-checking; Computer science; Context modeling; Encoding; Formal specifications; Information analysis; Object oriented modeling; Proposals; Unified modeling language;
Conference_Titel :
Computer Science, 2005. ENC 2005. Sixth Mexican International Conference on
Print_ISBN :
0-7695-2454-0
DOI :
10.1109/ENC.2005.52
