list of dots University of Ottawa logo / Université d'Ottawa

User Manual    [Previous]   [Next]   


Alloy is a formal method notation that can be used check properties of models using logic.

The Umple Alloy generator generates statements that can be used to analyse properties of class models involving associations. Both classes (with their attributes) and associations (with their multiplicity) are turned into sig statements in Alloy.

More information about Alloy can be found at the Alloy project home page, or on the Wikipedia Alloy page.

This generator is discussed in detail in Opeyemi Adesina's PhD thesis: Integrating Formal Methods with Model-Driven Engineering.