Version 0.52 of UML2Alloy uploaded. New version of the reference manual is also available.

A number of screencasts that show how UML2Alloy can be used were uploaded.

Version 0.51 of UML2Alloy uploaded. New version of the reference manual is also available.

New website and version 0.5 beta of UML2Alloy has been released. The new version of UML2Alloy is available in the downloads section.

UML2Alloy is the outcome of a research which attempts to formalise the Unified Modeling Language ( UML)* with the help of Alloy, using the Model Driven Architecture (MDA)* technology.

UML is the de facto modelling language that is used by the industry to model mainly software systems. UML is diagram based. OCL is a textual notation that is used to impose constraints over the UML model. However users of those notations are not able to reason about the soundness of their models, before the model is implemented. This happens because of the semi-formal nature of UML.

On the other hand users who are acquainted with formal methods are able to specify models in a formal notation (e.g. Z) and reason about certain properties. The drawback of formal methods is the fact that they are not easy to learn and understand.

UML2Alloy bridges this gap between the popularity and semi-formalism of UML. Using UML2Alloy users are able to use two critical functionalities of the Alloy Analyzer simulation and verification. Simulation ensures the model is not inconsistent and verification enables modellers to reason that certain critical properties of the model are satisfied.

The current version of UML2Alloy works on a subset of UML class diagrams enriched with OCL constraints.

* The UML and the MDA are registered trademarks of the OMG.