DocumentCode
3227980
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
fYear
2005
fDate
26-30 Sept. 2005
Firstpage
121
Lastpage
128
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Science, 2005. ENC 2005. Sixth Mexican International Conference on
ISSN
1550-4069
Print_ISBN
0-7695-2454-0
Type
conf
DOI
10.1109/ENC.2005.52
Filename
1592209
Link To Document