alloy

Relationship between Alloy and UML?


I am starting to learn Alloy and really like what I've seen.

Before encouraging my colleagues to join me in learning and using Alloy, I need to understand the relationship between Alloy and UML.

  1. Is Alloy a replacement of UML? If Alloy is used, then there is no need to use UML?
  2. Is Alloy complementary to UML? Is the recommended practice to use both Alloy and UML?
  3. Is Alloy orthogonal to UML? Alloy and UML have completely different purposes?
  4. In terms of functionality, is Alloy a superset of UML? From my reading I've learned that with the Alloy language one can express lots of constraints and then a SAT tool within Alloy can check the constraints against the model (created using Alloy). I "think" that UML tools, such as MagicDraw, do not have an equivalent capability for expressing constraints and assessing the UML model against the constraints -- is that correct?

In general, anything that you can tell me about the relationship (or lack of relationship) between Alloy and UML would be greatly appreciated.

Thank you.


Solution

  • Alloy is comparable to UML class diagrams augmented with OCL, UML’s constraint language. It doesn’t replace the other diagrams of UML.

    I’d recommend using Alloy for modeling data and for modeling behavior at a high level. For examples, see the Alloy website. You can always translate Alloy models into UML diagrams.

    Alloy is designed to offer — precise, succinct models of data rich designs — fully automatic analysis

    UML diagrams aren’t expressive enough for detailed modeling. The UML constraint language OCL does cover the same kinds of details as Alloy but does not have automated support to the same degree.

    The constraints in Alloy aren’t for checking the structure of a diagram, but for actually modeling a system and expressing its properties (and then you can check that the system satisfies the properties). Alloy is incomparable to OCL in expressiveness: OCL is more expressive in its treatment of arithmetic, but it lacks transitive closure, for example.

    I'm not very current with UML/OCL research, so perhaps someone in that area can chime in, but I can recommend that for more info on that you start with the work of Martin Gogolla's group, such as Mark Richters thesis on the semantics of OCL.

    If you search for "Alloy and UML" you'll find a bunch of papers about automatic translations from UML to Alloy, and comparison papers such as this one. We also wrote a paper way back about OCL and Alloy which probably criticizes OCL for things that have been fixed in the work of Richters et al.