Using Alloy to model-check visual design notations

13 years 10 months ago

Download www.utm.mx

This paper explores the process of validation for the 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 Formal specification, model checking, Alloy, visual modelling, UML

Anthony J. H. Simons, Carlos Alberto Fernán

Real-time Traffic

ENC 2005 | Graphical Notation | Keywords Formal Specification | Unified Specification |

claim paper

» Lessons learned using alloy to formally specify MLSPCA trusted security architecture

» Delegation Diagrams Visual Support for the Development of ObjectOriented Designs

» Surflex a programmable surface for the design of tangible interfaces

» The Role of Visual Tools in a Web Application Design and Verification Framework A Visual N...

» Model checking SystemC designs using timed automata

» 3D Form Display with Shape Memory Alloy

» Automating commutativity analysis at the design level

» A Minimalist Visual Notation for Design Patterns and Antipatterns

Post Info
More Details (n/a)

Added	24 Jun 2010
Updated	24 Jun 2010
Type	Conference
Year	2005
Where	ENC
Authors	Anthony J. H. Simons, Carlos Alberto Fernández y Fernández

Comments (0)

Sciweavers

Using Alloy to model-check visual design notations

ENC 2005 | Graphical Notation | Keywords Formal Specification | Unified Specification |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers