Why create a model using Alloy?
I believe that I know the answer, but I want to confirm with you.
We create a model using Alloy because we want to verify that the model holds for some property. Please allow me to give a few examples to illustrate what I mean:
- We create an Alloy model of a traffic light system because we want to verify that the traffic light system will never have two green lights (in perpendicular directions) at a junction at the same time. By building an Alloy model and checking it using the Alloy Analyzer, we can verify that the traffic light system is safe.
- We create an Alloy model of a leader election protocol (in a bunch of decentralized, communicating processes one process is elected the leader) because we want to verify that the protocol results in electing exactly one process as the leader.
- We create an Alloy model of a hotel’s operations because we want to verify that there will be no unauthorized access to any room.
Those examples illustrate why we create Alloy models: so we can verify that some property holds. After creating the Alloy model and verifying that the desired property holds, if we faithfully implement the model then we can have confidence that the system will have the desired property. That’s why we create Alloy models. Do you agree? Is there anything else you would add?
I think the primary reason for Alloy is to provide a modeling language. In Alloy, you can define the core structure of a problem or algorithm. Since the tool can provide feedback about this model you learn quickly what you misunderstood of the problem in the first place.
Second, it is a specification language. If you look at for example Javadoc then you see that the semantics of an API are comments. In Alloy, you can actually define more of those semantics in a way that is not possible to interpret in different ways. It is easy to state invariants and post conditions. For example, in a blog post I defined a few operations in the Java Map. The interesting thing is that modeling this showed how important the null key and value aspect is of Java maps. This hardly gets any mention in the Javadoc.
Last, you can use Alloy to check the properties of a system, as you indicated. I recently did find a case in a concurrent problem using Alloy. However, in general once you found it you work it into the model.